Alloy2JML
Java Modeling Language (JML) is a specification language for Java programs, that follows the design by contract paradigm. It is not always easy to use JML, however—for example when specifying properties of linked data structures. Alloy, on the other hand, is a relational specification language with a built-in transitive closure operator which makes it particularly suitable for writing concise specifications of linked data structures. This paper presents Alloy2JML, a tool that translates Alloy specifications of Java programs to JML, in order to support both Alloy and JML specifications in the KeY verification engine. This translation allows Java programs with Alloy specifications to be fully verified for correctness. Moreover, Alloy2JML lets Alloy specifications be employed in a variety of tools that accept only JML as their specification language. It also enables users to validate specifications before using them.
publications
- Translating Alloy Specifications to JML, Daniel Grunwald, Christoph Gladisch, Tianhai Liu, Mana Taghdiri, and Shmuel Tyszberowicz, HVC 2014
- Translating Alloy Specifications to JML, Daniel Grunwald, Master Thesis, KIT, Dec. 2013
people
- Mana Taghdiri
- Shmuel Tyszberowicz
- Christoph Gladisch
- Daniel Grunwald
- Tianhai Liu
Tool
Experiments
To evaluate our translation, we have applied Alloy2JML to 6 methods of two Java classes: Linked List and Binary Search Tree. The following file contains Java code with Alloy specifications, the translation to JML by Alloy2JML, and manually written lemmas for conducting proofs in the KeY verification tool.