Automated Software Analysis Group

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

 


people

  • Mana Taghdiri
  • Shmuel Tyszberowicz
  • Christoph Gladisch
  • Daniel Grunwald
  • Tianhai Liu

Tool

If you are interested in the Alloy2JML, please contact Mana Taghdiri.


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.

 experiments.zip