Checking JML Specifications with B Machines - Archive ouverte HAL Access content directly
Conference Papers Year : 2005

Checking JML Specifications with B Machines

(1) , (1) , (2)
1
2

Abstract

This paper presents a solution to the lack of tool-support for the JML models verification. We propose an approach for expressing JML specifications within the B abstract machines notation. The B machines generated from the JML can then be checked to ensure their correctness. Thus, we deduce the correctness of the original JML specification, ensured by rewriting rules which give the semantical equivalence of the two models. More generally, this translation can be applied to object-oriented specification languages using before-after predicates.

Dates and versions

inria-00329986 , version 1 (13-10-2008)

Identifiers

Cite

Fabrice Bouquet, Frédéric Dadeau, Julien Groslambert. Checking JML Specifications with B Machines. International Conference on Formal Specification and Development in Z and B - ZB'05, Apr 2005, Guildford, United Kingdom. pp.434-453, ⟨10.1007/b135596⟩. ⟨inria-00329986⟩
122 View
0 Download

Altmetric

Share

Gmail Facebook Twitter LinkedIn More