Daniel Grunwald, Christoph Gladisch, Tianhai Liu, Mana Taghdiri, Shmuel Tyszberowicz
10th Haifa Verification Conference (HVC), 2014
Abstract
Java Modeling Language (JML) is a specification language for Java programs, that follows the design by contract paradigm. However, it is not always easy to use JML, 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 generates JML specifications from Alloy expression, 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. Supporting Alloy has the additional advantage that users can validate the specifications beforehand using the Alloy Analyzer.
@InProceedings{grunwald-gladisch-Liu-Taghdiri-Tyszberowicz-2014,
author = {Daniel Grunwald and Christoph Gladisch and Tianhai Liu and Mana Taghdiri and
Shmuel Tyszberowicz},
title = {Generating JML Specifications from Alloy Expressions},
booktitle = {10th Haifa Verification Conference (HVC), 2014},
year = {2014},
month = {November}
}