A Specification Language Design for the Java Modeling Language (JML) 
        Using Java 5 Annotations
				          by
		      Kristina B. Taylor

			       Abstract

Design by contract specification languages help programmers write their 
intentions for a piece of code in a formal mathematical language.  Most 
programming languages do not have built-in syntax for such specifications, 
so many design by contract languages place specifications in comments.  
The Java Modeling Language (JML) is one such specification language for 
Java that uses comments to specify contracts.  However, starting with version 
5, Java has introduced annotations, a syntactical structure to place metadata 
in various places in the code.  This thesis proposes an initial design to 
writing JML contracts in the Java 5 annotation syntax and evaluates several 
criteria in the areas of specification languages and Java language design: 
whether these annotations are expressive enough to take advantage of annotation 
simplicity and tool support, and whether the annotation syntax is expressive 
enough to support handling a large specification language such as JML.

Keywords: JML, 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
All rights reserved.