Desugaring JML Method Specifications
				  by
		 Arun D. Raghavan and Gary T. Leavens

			       Abstract

JML, which stands for ``Java Modeling Language,'' is a behavioral
interface specification language (BISL) designed to specify Java
modules.  JML features a great deal of syntactic sugar that is
designed to make method specifications more expressive.  This paper
presents a desugaring process that boils down all of the syntactic
sugars in JML method specifications into a much simpler form.  This
desugaring will help one understand the meaning of these sugars, for
example for use in program verification.  It may also help
manipulation of JML method specifications by tools.


Keywords: Behavioral interface specification language,
 formal specification, desugaring, semantics,
 specification inheritance, refinement, behavioral subtyping,
 model-based specification, formal methods,
 precondition, postcondition, Eiffel, Java, JML.

1999 CR Categories:
D.2.4 [Software Engineering] Software/Program Verification
       --- Formal methods, programming by contract, reliability, tools,
	   JML;
D.2.7 [Software Engineering] Distribution, Maintenance, and Enhancement
       --- Documentation;
F.3.1 [Logics and Meanings of Programs]
       Specifying and Verifying and Reasoning about Programs ---
        Assertions, pre- and post-conditions,
        specification techniques;

Copyright (c) 2000, 2001, 2003 by Arun D. Raghavan and Gary T. Leavens.