How the Design of JML Accommodates
		   Both Runtime Assertion Checking
		       and Formal Verification
				  by
Gary T. Leavens, Yoonsik Cheon, Curtis Clifton, Clyde Ruby, and David R. Cok

			       Abstract

Specifications that are used in detailed design and in the
documentation of existing code are primarily written and read by
programmers.  However, most formal specification languages either make
heavy use of symbolic mathematical operators, which discourages use by
programmers, or limit assertions to expressions of the underlying
programming language, which makes it difficult to write complete
specifications.  Moreover, using assertions that are expressions in
the underlying programming language can cause problems both in runtime
assertion checking and in formal verification, because such
expressions can potentially contain side effects.  The Java Modeling
Language, JML, avoids these problems.  It uses a side-effect free
subset of Java's expressions to which are added a few mathematical
operators (such as the quantifiers \forall and \exists).  JML also
hides mathematical abstractions, such as sets and sequences, within a
library of Java classes.  The goal is to allow JML to serve as a
common notation for both formal verification and runtime assertion
checking; this gives users the benefit of several tools without the
cost of changing notations.


Keywords: specification languages, runtime assertion checking,
documentation, tools, formal methods, program verification,
programming by contract, Java language, JML language, Eiffel language,
Larch family of specification languages.

2000 CR Categories: 
D.2.1 [Software Engineering]
        Requirements/Specifications --- languages, tools, JML;
D.2.2 [Software Engineering]
        Design Tools and Techniques --- modules and interfaces,
        object-oriented design methods;
D.2.4 [Software Engineering]
        Software/Program Verification --- Assertion checkers,
        class invariants, correctness proofs, formal methods,
        programming by contract, reliability, tools, validation, JML;
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, logics of programs, mechanical
        verification, pre- and post-conditions, specification techniques;

This is a slightly corrected version of the paper that appears in
Frank S. de Boer, Marcello M. Bonsangue, Susanne Graf, and
Willem-Paul de Roever (eds.), Formal Methods for Components and
Objects, pages 262-284.  Volume 2852 of Lecture Notes in Computer
Science, Springer Verlag, Berlin, 2003.

Copyright (c) 2003 Springer Verlag.