Adapting the Java Modeling Language for Java 5 Annotations
				  by
           Kristina B. Taylor, Johannes Rieken, and Gary T. Leavens

			       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. 

Keywords: JML, Modern Jass, Java, specification, annotation

2008 CR Categories:
D.2.1 [Software Engineering]
        Requirements/Specifications --- languages, tools, JML;
D.2.2 [{\em Software Engineering\/}]
        Design Tools and Techniques --- 
                computer-aided software engineering (CASE);
D.2.4 [Software Engineering]
        Software/Program Verification --- Assertion checkers,
                class invariants, formal methods, programming by contract,
                reliability, tools, validation, JML;
F.3.1 [Logics and Meanings of Programs]
       Specifying and Verifying and Reasoning about Programs ---
        Assertions, invariants, pre- and post-conditions,
        specification techniques.

Copyright (c) 2008 by Kristina B. Taylor, Johannes Rieken, and Gary T. 
Leavens
All rights reserved.