Lessons from the JML Project
				  by
		  Gary T. Leavens and Curtis Clifton

			       Abstract

To have impact, a grand challenge should provide a way for diverse
research to be integrated in a synergistic fashion.  Synergy in the
JML project comes from a shared specification language, and thus holds
several lessons for the verifying compiler grand challenge.  An
important lesson is that the project should focus considerable
resources on specification language design, which still contains many
open research problems.  Another important lesson is that, to support
such a specification language, the project needs to involve groups
doing research on extensible compilers and integrated development
environments.

Keywords: verifying compiler, specification, verification, formal methods,
formal interface specification, extensible compilers, integrated
development environments, JML language, Java language, Hoare

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,
                testing tools, theory;
F.3.1 [Logics and Meanings of Programs]
        Specifying and Verifying and Reasoning about Programs ---
                Assertions, invariants, pre- and post-conditions,
                specification techniques.