Leavens, Gary T., Leino, K. Rustan M., Poll, Erik, Ruby, Clyde and Jacobs, Bart (2000) JML: notations and tools supporting detailed design in Java. Technical Report TR00-15, Department of Computer Science, Iowa State University.
JML: notations and tools
supporting detailed design in Java
Gary T. Leavens, K. Rustan M. Leino, Erik Poll,
Clyde Ruby, and Bart Jacobs
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,
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.
Contact site administrator at: firstname.lastname@example.org