Translating Alloy Specifications to JML
-
Author:
Daniel Grunwald
-
Place:
Karlsruhe Institute of Technology, Master thesis, 2013
- Date: November 2013
-
Abstract
The lightweight Alloy specification language has been used for the specification of Java programs in the context of test-case generation and bounded verification. The aim of this thesis is the design of an automatic translation from Alloy into the Java Modeling Language (JML). Our tool "Alloy2JML" transforms relational Alloy formulas into JML expressions that represent relations using first-order logic. We use a translation function that has existential semantics and is defined recursively over the Alloy syntax tree. It is followed by a series of simplification steps that help remove redundant quantifiers introduced by the translation. The transitive closure operator is translated into recursively specified model methods.
The translation into JML allows the usage of JML tools on the input programs using Alloy specifications. We use the KeY theorem prover on the output of the translation to verify the correctness of two example programs.
The translation of a subset of the Alloy language is formally proven correct using the Isabelle theorem prover.