What should I download?
Consider using OpenJML from github.com first. The download is available from its releases page. User information and a tutorial are available from the OpenJML GitHub Pages site (www.openjml.org).
KeY is another alternative for JML. It can be downloaded from the KeY Project download page. (See the KeY Quicktour for JML.)
Users might also try one of the following tools:
- The AspectJML tool is able to specify and do runtime assertion checking for both Java and AspectJ programs. Ajmlc uses aspect-oriented compilation techniques to provide significantly improved runtime assertion violation messages, and also works with JavaME.
- The
jml4c tool is a JML compiler built on the Eclipse Java
compiler. It translates a significant subset of JML specifications
into runtime checks. Notable features of JML4c include
(1) support for Java 5 features such as generics
and enhanced
forloops, (2) support for nested classes, (3) improved compilation speed, and (4) improved error messages. Using JML4c, one can now verify Java 5 classes annotated with JML specifications. - Sireum/Kiasan for Java, which is a JML contract-based automatic verification and test case generation tool-set for Java program units.
- JmlOk2 is a tool that uses random tests to check Java code against JML specifications and suggest likely causes for non-conformance problems it finds.
Downloading Other Tools for JML
The following JML-related tools may also be useful:- The JACK: Java Applet Correctness Kit environment can be obtained from its download page.
- The Daikon invariant detector project from the University of Washington's Programming Languages and Software Engineering Group.
- AutoJML was a tool for the generation of JML specifications from state diagrams in various formats (including UML diagrams) and from security protocol specifications.
- JForge, a front-end to the Forge bounded verification library, automatically analyzes Java code against full JML specifications.
- Modern Jass, is a design by contract tool that worked with Java 5 and was closely related to JML.
Last modified Friday, December 10, 2021.