(thanks to Robert Atkey)
The website http://www.jmlspecs.org/
is the main source for JML information.
Other assorted papers
and links on JML
- Reassessing JML's Logical Foundation
by Patrice Chalin. Discusses whether to change JML's underlying logic
to a three-valued logic in order to cope with exceptions. Describes the
results of a survey of software developers on what the expected value
of specification expressions containing errors should be.
A paper summarising some of the tools below: An overview of JML tools and applications.
: The Iowa State JML tools
jml, the JML syntax and type checker;
jmlc, the runtime assertion checker;
the unit tester; and
jmldoc, the extension of
for formating JML annotations in documentation.
- Compiling this yourself from CVS is a pain since it relies
a multi-methods extension to Java, but it is easy enough to use the
- http://secure.ucd.ie/products/opensource/ESCJava2/ :
- This is the new version of the original ESC/Java,
upgraded to support more of JML and Java 1.4. See ESC/Java2 Implementation Notes, chapter 5 for
information on the changes.
- Reads JML-annotated Java code and attempts to satisfy the
generated verification conditions
- Uses the Simplify automatic theorem prover also available
from hp labs. Written in Modula-3, using the PM3 compiler.
- Intends to move from using Simplify (out-of-date apparently)
to using the generic syntax from the SMT-Lib
: Krakatoa system
- Reads JML-annotated Java code and produces verification
- Uses Why as
generic VCG. Can output to Coq, PVS, Isabelle/HOL, HOL4, HOL Light,
Mizar and some automatic systems: Simplify (as used by ESC/Java2), CVC
Lite and haRVey.
Pierangelo Miglioli's web page