The Java Modeling Language (JML) Download Page

What should I download?

Users who are willing to work with Java 1.4 source files (no generics, or other Java 1.5+ features), and who want to use Eclipse (with JDK 1.4, 1.5, or 1.6), should consider first using the Mobius Program Verification Environment. It includes several JML tools (ESC/Java2, JML2, and a variety of other static checkers and verification tools), and it works on Linux, Mac OS X, and Windows. (Many of the tools only work with Java 1.4 source files, but some others work with Java 1.5 and later.)

Users who want to work with Java 1.5 or 1.6 sources should consider the following tools:

OpenJML, a new pre-alpha version of the JML tool-suite developed on top of the OpenJVM compiler infrastructure,
The jml4c tool is a new 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 for loops, (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,
Modern Jass, is a design by contract tool that works with the latest versions of Java and is closely related to JML, or
JMLEclipse, which is a pre-alpha version of the JML tool-suite developed on top of Eclipse's JDT compiler infrastructure.

Only hardcore developers who are comfortable with compilers and Eclipse should consider using OpenJML and JMLEclipse at this time (November 2009).

Downloading Other Tools for JML

Aside from the Common (formerly ISU) JML tools (see below), other tools for JML can be obtained from the page of others working on JML tools. In particular:

The Mobius Program Verification Environment can be downloaded for use with Eclipse. It includes several JML tools and works on Linux, Mac OS X, and Windows.
ESC/Java2 can be downloaded by following the instructions on the ESC/Java2 download web page.
The ajmlc tool is good substitute for the JML2 runtime assertion checker. Ajmlc uses aspect-oriented compilation techniques to provide significantly improved runtime assertion violation messages, and also works with JavaME.
The ESC/Java2 plugin for Eclipse can be obtained or updated from inside Eclipse, using the Mobius update site: http://kind.ucd.ie/products/opensource/Mobius/updates/.
The JML2 Eclipse plugin provides a basic integration of the Common JML tools into Eclipse, and can be downloaded from ETHZ's website.
The Translation of Annotated COde (TACO) tool, which statically checks the compliance of a Java program against its JML specification, using a bounded verification technique.
Sireum/Kiasan for Java, which is a JML contract-based automatic verification and test case generation tool-set for Java program units.
The JACK: Java Applet Correctness Kit environment can be obtained from its download page.
Daikon can be downloaded from the Daikon download page.
KeY can be downloaded from the KeY Project download page. (See the KeY Quicktour for JML.)
AutoJML is 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.
CoJava, a tool that generates code for CoJava's concurrency model and translates it into JML.
Modern Jass, is a design by contract tool that works with the latest versions of Java and is closely related to JML.

Downloading the Common (formerly ISU) JML Tools

The Common (formerly ISU) JML tools release is currently in beta-test. It runs on any platform that has J2SDK 1.4.1 or J2SDK 1.4.2. We have tested it on Red-Hat Linux, Windows XP, and Mac OSX.

You can get the latest release of the Common JML tools by following the steps below.

Fetch the release from the following URL http://sourceforge.net/projects/jmlspecs/ or more directly from http://sourceforge.net/project/showfiles.php?group_id=65346. (If those links are down, you can also download the Common JML tools from http://www.jmlspecs.org/OldReleases/.) You will be getting a gzipped tar file, such as JML.5.2.tar.gz.
You now have the gzipped tar archive.
Under Windows, use Winzip or some similar program to extract it to some directory of your choice. For example, use Winzip to extract it to c:\.
On Unix, you might use the following commands to untar it, after saving it to /usr/local/JML.tgz.
```
cd /usr/local
      tar -xzvf JML.5.2.tar.gz
```
Now, using a web browser, read the file JML/README.html in what you just unpacked for further instructions.

If you have trouble with these instructions, please file a support request through the sourceforge.net support tracker interface so we can try to help you. (You have to get a sourceforge.net login first, but that just allows us to contact you. To get a login, use the 'New User via SSL' link, located near the top of the left navigation bar on the SourceForge.net site.)

We are also interested in your feedback on JML: things you like, don't like, find confusing, etc. Since JML is open source, we'd appreciate it if you'd send us any bug fixes or enhancements you are willing to share with others. See the sourceforge.net tracker interface for places to file bug reports, support requests, patches, and feature requests for JML and its tools.

After installation, please either register with sourceforge to be notified of future file releases for JML (by clicking on the little envelope in the file section of the sourceforge project page, or if you don't have a sourceforge.net login, by signing up for the mailing list jmlspecs-releases@lists.sourceforge.net through its SourceForge.net web interface. This will let us inform you of future releases.

You can also get access to the JML sources from the SourceForge.net project page for JML

Last modified Friday, May 14, 2010.