JML

The Java Modeling Language (JML) is a language used to describe the functional behavior of Java classes and methods. The descriptions of behavior are expressed as structured Java comments or Java annotations that use Java-like logical expressions. Various tools can then read the JML information and do static checking, runtime checking, test generation, display for documentation, or other useful tasks.

More information about JML can be found on the JML web site. The information includes publications, groups using or contributing to JML, mailing lists, etc. There is also a GitHub project, this general documentation site, and a wiki for OpenJML developers.

The old sourceforge site at https://jmlspecs.sourceforge.net is now obsolete and not maintained, except as a download site. Also the sourceforge project, while currently still used for JML material, is no longer used for OpenJML, which has moved to GitHub.

OpenJML

OpenJML is a tool set for JML, built on the OpenJDK framework for Java. It is intended as the replacement for ESC/Java2, which is only for Java 1.4. OpenJML is current with Java 1.8. This page makes available some resources for OpenJML and links give information about installing and running OpenJML.

Note that OpenJML is not a theorem prover or model checker itself. OpenJML translates JML specifications into SMT-LIB format and passes the proof problems implied by the Java+JML program to backend SMT solvers. Success in checking the consistency of the specifications and the code will depend on

The key goal of OpenJML is to implement a full tool for JML that is easy for practitioners and students to use to specify and verify Java programs. In addition, however, and corresponding to the points above, other goals of OpenJML are to provide challenge problems to SMT solvers (point a), particularly around quantified expressions, to experiment with the encoding of code and specifications in OpenJML itself (point b) and to allow users to easily experiment with styles of specification writing (point c).

A summary of the features and the implementation status of OpenJML is here.

Note that OpenJML requires Java 1.8 to run (and in particular one based on OpenJDK); it will not operate with Java 9. [OpenJML uses components of OpenJDK 1.8 and consequently must be run in the context of the rest of OpenJDK 1.8.] Such builds can be obtained from the Oracle release site. The source code for OpenJML is kept in github as a module of the OpenJML GitHub project. The JMLAnnotations and Specs projects (also modules of that project) are used by OpenJML.

Documentation

The OpenJML user guide is part of the download, but is also available here (as pdf) and as html (or as one frame-less HTML page). There is also an online quick-start user guide.

Command-line tool

The OpenJML command line tool can be downloaded as a tar.gz file or a zip file.

Eclipse plug-in

The Update site for the Eclipse plug-in that encapsulates the OpenJML tool is http://jmlspecs.sourceforge.net/openjml-updatesite.

Development of OpenJML

Developers contributing to OpenJML should refer to the OpenJML wiki.