Adapting the Java Modeling Language for Java 5 Annotations

Date
2008-04-01
Authors
Taylor, Kristina
Rieken, Johannes
Leavens, Gary
Journal Title
Journal ISSN
Volume Title
Publisher
Altmetrics
Authors
Research Projects
Organizational Units
Computer Science
Organizational Unit
Journal Issue
Series
Abstract

The Java Modeling Language (JML) is a formal specification language for Java that allows to express intended behavior through assertions. Currently, users must embed these assertions in Java comments, which complicates parsing and hinders tool support, leading to poor usability. This paper describes a set of proposed Java 5 annotations which reflect current JML assertions and provides for better tool support. We consider three alternative designs for such annotations and explain why the chosen design is preferred. This syntax is designed to support both a design-by-contract subset of JML, and to be extensible to the full language. We demonstrate that by building two tools: Modern Jass, which provides almost-native support for design by contract, and a prototype that works with a much larger set of JML.

Description
Keywords
JML, Modern Jass, Java, Specification, Annotation
Citation
DOI
Source
Collections