Discussion of Design Alternatives for JML Java 5 Annotations
				  by
		Kristina P. Boysen and Gary T. Leavens

			       Abstract

The Java Modeling Language (JML) is a specification language for Java
that allows users to specify intended code behavior through assertions
attached to the code. Currently, these assertions are written in Java
comments in the code. This paper describes a proposed syntax for
translating the current JML assertions into new Java 5 annotations. 
This would allow syntax checkers in tools like Eclipse to check 
part of the assertion syntax and give code completion assistance
to the user.

Keywords: JML, Java, Specification, Annotation.

2006 CR Categories:
D.2.1 [Software Engineering]
        Requirements/Specifications --- languages;
D.3.1 [Software Engineering] Software/Program Verification
       --- Formal methods, programming by contract, reliability, tools, JML;
F.3.1 [Logics and Meanings of Programs]
       Specifying and Verifying and Reasoning about Programs ---
        Assertions, pre- and post-conditions,
        specification techniques;

Copyright (c) 2008 by Kristina P. Boysen and Gary T. Leavens
All rights reserved.