JML: notations and tools
		  supporting detailed design in Java
				  by
	  Gary T. Leavens, K. Rustan M. Leino, Erik Poll,
		     Clyde Ruby, and Bart Jacobs


			       Abstract


JML is a notation for specifying the detailed design of Java classes
and interfaces.  JML's assertions are stated using a slight extension
of Java's expression syntax.  This should make it easy to use.  Tools
for JML aid in static analysis, verification, and run-time debugging
of Java code.


Keywords: Behavioral interface specification language, detailed design
notation, Java language, JML language, ESC/Java, LOOP.


1999 CR Categories:
D.2.1 [Software Engineering]
        Requirements/Specifications --- languages, tools, JML,
        ESC/Java, LOOP;
D.2.4 [Software Engineering]
        Software/Program Verification --- Class invariants,
        correctness proofs, 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, invariants, logics of programs,
        pre- and post-conditions, specification techniques;

To appear in OOPSLA 2000 Companion, Minneapolis, Minnesota,
Copyright (c) ACM 2000.