OpenJML

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. MacOSX releases can be obtained from Dan Zimmerman's site.

Documentation

The OpenJML user guide is part of the download, but is also available here.

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.

The general instructions for setting up a development environment are found on the JML wiki.