A Runtime Assertion Checker for the Java Modeling Language (JML)
				  by
		  Yoonsik Cheon and Gary T. Leavens

			       Abstract

Debugging is made difficult by the need to precisely describe what
each piece of the software is supposed to do, and to write code to
defend modules against the errors of other modules; if this is not
done it is difficult to assign blame to a small part of the program
when things go wrong. Similarly, unit testing also needs precise
descriptions of behavior, and is made difficult by the need to write
test oracles. However, debugging and testing consume a significant
fraction of the cost of software development and maintenance efforts.
Inadequate debugging and testing also contribute to quality problems.
We describe a runtime assertion checker for the Java Modeling Language
(JML) that helps in assigning blame during debugging and in automatic
generation of test oracles. It represents a significant advance over
the current state of the art, because it can deal with very abstract
specifications which hide representation details, and other features
such as quantifiers, and inheritance of specifications. Yet JML
specifications have a syntax that is easily understood by
programmers. Thus, JML's runtime assertion checker has the potential
for decreasing the cost of debugging and testing. 


Keywords: runtime assertion checking, formal methods, formal
interface specification, programming by contract, JML language, Java
language 


2000 CR Categories:
D.2.1 [Software Engineering]
        Requirements/ Specifications --- languages, tools, JML;
D.2.2 [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;
D.2.5 [Software Engineering]
        Testing and Debugging --- Debugging aids, design, monitors, 
                testing tools, theory;
D.3.2 [Programming Languages]
        Language Classifications --- Object-oriented languages;
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) 2002 by Yoonsik Cheon and Gary T. Leavens.