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.

OpenJML is a command-line tool that has the following capabilities:

  • 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
Other features that are in development include
  • integration with IDEs like IntelliJ and Eclipse,
  • 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.

OpenJML is intended to replace the original JML2 tools developed at ISU (which only worked through Java 1.4).

Contacts

  • The principal developer of OpenJML is David Cok
  • For general information about JML, contact an appropriate JML mailing list. See the list at sourceforge; in particular jmlspecs-interest@lists.sourceforge.net.
  • You can also contact people listed on the JML web site. A sub-page acknowledges the many people that have contributed in various ways to JML.

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:

  • Gary Leavens, for collaboration on JML syntax and semantics, as well as bug reports and sponsoring senior design teams
  • 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 Aggarwal (GrammaTech engineer) for reworking the organization of OpenJML testing
  • Joshua Robbins (NSF REU intern at GrammaTech) for debugging and testing
  • Daniel Houck (Harvey-Mudd undergraduate, under Dan Zimmerman) for the initial implementation of syntax coloring
  • John Singleton, through his Ph.D. thesis
  • Various senior design teams and student contributors at UCF
  • all those that communicated bug reports and tested fixes

Acknowledgements

The majority of the work of the project has been (and is being) provided by volunteers. Some financial and grant support has been provided by the following sources:
  • aicas provided an equipment grant.
  • NSF grant CCF0916350 supported some of Gary Leavens and John Singleton’s work.
  • NSF Grant ACI-1314674 supported some of David Cok’s work.
  • Work on some improvements and bug fixes was supported by AWS.
  • Work on some improvements and bug fixes was supported by Goldman-Sachs R&D.
  • Work on some improvements and bug fixes and documentation was supported by CEA (France).
NSF Disclaimer: This material is based upon work supported by the National Science Foundation under the grants listed above. Any opinions, findings, and conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the views of the National Science Foundation.