Introduction to OpenJML

About OpenJML

OpenJML is a suite of tools for editing, parsing, type-checking, verifying (static checking), and run-time checking Java programs that are annotated with JML statements stating what the program's methods are supposed to do and the invariants the data structures should obey. JML annotations state preconditions, postconditions, invariants and the like about a method or class; OpenJML's tools will then check that the implementation and the specifications are consistent.

The Java Modeling Language (JML) is a behavioral interface specification language (BISL) that can be used to specify the behavior of Java modules. It combines the design by contract approach of Eiffel and the model-based specification approach of the Larch family of interface specification languages, with some elements of the refinement calculus. There is a web site for JML here, including a Reference Manual [PDF] [postscript], references to key publications, links to groups that contribute to or use JML, and other documentation.

OpenJML has the following capabilities:

Other features that are in development include


OpenJML is developed by David Cok. It is based on JML, the OpenJDK compiler, Eclipse plug-ins, and SMT-lib based SMT solvers, all of which have had countless other people contributing to them.

The following have also contributed to OpenJML in various ways: