Description
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).