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 intends to be current with current Java. 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.
Current OpenJML does not require an installation of Java to run. The source code for OpenJML is kept in github as a module of the OpenJML GitHub project. The JMLAnnotations, Specs, and Solvers projects (also modules of that project) are used by OpenJML.
OpenJML is a command-line tool (plugins for Eclipse and IntelliJ are in progress).Development of OpenJML
Developers contributing to OpenJML should refer to the OpenJML wiki.