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:
- a command-line tool that enables
- parsing and type-checking of Java+JML programs
- static checking of JML annotations using backend SMT solvers
- runtime-assertion checking, using an extension of the OpenJDK Java compiler
- an Eclipse plug-in that
- encapsulates the capabilities of the command-line tool in an Eclipse GUI that provides many UI features appropriate to JML annotations
- permits interactively exploring counter-examples resulting from failed attempts to verify assertions
- a programmatic API that gives programmatic access to the command-line tool capabilities from Java programs
- generation of javadoc documentation embellished with JML information,
- generation of annotation templates,
- inference of specifications from implementations,
- and auto-generation of test cases using symbolic execution, guided by JML annotations.
People
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:
- John Singleton (UCF< with Gary Leavens)
- Dan ZImmerman, Marieke Huisman, Wojciech Mostowski, Arend Rensink and others for usability suggestions and bugs while preparing course materials
- Gunjan Aggarawal (GrammaTech engineer) for reworking the organization of OpenJML testing
- Daniel Houck (Harvey-Mudd undersgraduate, under Dan Zimmerman) for the initial implementation of syntax coloring
- all those that communicated bug reports and tested fixes
Last modified Nov 14 2025.