A Run-time Assertion Checker for Java using JML
				  by
			    Abhay Bhorkar

			       Abstract

The Java Modeling Language (JML) is a behavioral interface
specification language tailored for specifying Java modules. This
paper describes a source-to-source translation tool that takes a JML
specification and Java source code for a module and produces source
code that checks assertions at run-time. It describes issues unique to
JML, including specification-only variables, refinement, specification
inheritance, and privacy. It also describes the design and
implementation of the translation tool.


Keywords: run-time assertion checking, precondition checking,
model-based specification, behavioral interface specification
language, behavioral subtyping, refinement, formal specification
languages, Eiffel, JML, Java.

1999 CR Categories:
D.2.1 [Software Engineering]
        Requirements/Specifications --- languages, tools, JML;
D.2.4 [Software Engineering]
        Software/Program Verification --- Assertion checkers, class invariants,
        formal methods,
        programming by contract, reliability, tools, JML;
D.2.5 [Software Engineering]
        Testing and Debugging --- Debugging aids;
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) 2000 by Iowa State University