Abstract
This paper introduces a tool, named JML2B, destined to check the consistency of JML specifications. JML2B is a solution to the lack of tool-support for the JML models verification. Our tool translates JML specifications into the B abstract machines notation. The generated B machines can then be checked to ensure their correctness. When the proof fails, it is possible to retrieve the mistakes in the original JML specification.
Cite
CITATION STYLE
Bouquet, F., Dadeau, F., & Groslambert, J. (2006). JML2B: Checking JML specifications with B machines. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4355 LNCS, pp. 285–288). Springer Verlag. https://doi.org/10.1007/11955757_31
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
