This sourceforge site is obsolete -- all current work is on GitHub at github.com/OpenJML .
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 sourceforge project, including a wiki for JML.
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.7u40. 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
- (a) the capability of the backend SMT solver,
- (b) the particular encoding of code+specifications into SMT by OpenJML, and
- (c) the complexity and style in which the code and specifications are written.
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.7 to run (and in particular one based on OpenJDK); it will not operate with Java 8. [OpenJML uses components of OpenJDK 1.7 and consequently must be run in the context of the rest of OpenJDK 1.7.] Such builds can be obtained from the Oracle release site. The source code for OpenJML is kept in sourceforge as a module of the JML Project. The JMLAnnotations and Specs projects (also modules of JML) are used by OpenJML. Information about creating a developer's environment for the OpenJML source can be found below.
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 can retrieve a project-set file to download source code from SVN and create the corresponding projects within Eclipse from here.
Alternately, the set of SVN commands needed to checkout all the pieces of the OpenJML source code into the directory structure expected by Eclipse (or to be used by some other tool) is here.
The general instructions for setting up a development environment are found on the JML wiki.
Last modified Nov 14 2025.