JML stuff 

The website http://www.jmlspecs.org/ is the main source for JML information.

JML itself

• Preliminary Design of JML: A Behavioural Interface Specification Language for Java (HTML version). A tutorial introduction to the design of JML. Includes lots of examples. PDF version.
• JML Reference Manual (HTML version). The main reference work on the design of JML. More detailed than the previous document. PDF version.

Other assorted papers and links on JML

• Two papers on how to axiomatise pure functions used in JML specifications: Reasoning with specifications containing method calls in JML by David Cok, this describes how ESC/Java2 translates the specification of pure methods into the logic of Simpilfy. Reasoning About Method Calls in JML Specifications by Adam Darvas and Peter Müller, this paper points out the unsoundness of the previous paper's approach and describes another technique that is proven sound, consistent and deals with weak purity.

• 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.

• The Formal Techniques for Java-like Programs workshop contains a lot of material relevant to JML.

Software Tools

A paper summarising some of the tools below: An overview of JML tools and applications. 

• http://www.cs.iastate.edu/~leavens/JML//download.shtml : The Iowa State JML tools
  • Includes jml, the JML syntax and type checker; jmlc, the runtime assertion checker; jmlunit, the unit tester; and jmldoc, the extension of javadoc for formating JML annotations in documentation.
  • Compiling this yourself from CVS is a pain since it relies on MultiJava, a multi-methods extension to Java, but it is easy enough to use the binary distribution.

• http://secure.ucd.ie/products/opensource/ESCJava2/ : ESC/Java2
  • 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 project.

• http://pag.csail.mit.edu/daikon/ : Daikon invariant detector
  • monitors running Java code to guess at suitable invariants

• http://krakatoa.lri.fr/ : Krakatoa system
  • Reads JML-annotated Java code and produces verification conditions
  • Uses Why as a 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.

• http://key-project.org/ : The KeY project

• http://www-sop.inria.fr/everest/soft/Jack/jack.html : JACK -- Java Applet Correctness Kit
  • Developed by Gemplus and INRIA
  • Not publicly available

OCL

Pierangelo Miglioli's web page