JML
The Java Modeling Language (JML) is a language that enables logical assertions to be made about Java programs. The assertions are expressed as structured Java comments or Java annotations. Various tools can then read the JML information and do static checking, runtime checking, 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 for JML.
OpenJML
OpenJML is a tool set for JML, built on the OpenJDK framework for Java. OpenJML is current with Java 1.7. This page makes available some resources for OpenJML. OpenJML is a work in progress.
A summary of the features and the implementation status of OpenJML is here.
Note that OpenJML requires an OpenJDK build of Java 1.7 to run. 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. There is also an online user guide. These documents are works in progress.
Command-line tool
The OpenJML command line tool can be downloaded from here.
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 on 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 is here.
The general instructions for setting up a development environment are found on the JML wiki.
Last modified 2013 May 11.