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
Other features that are in development include
  • 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). There are no other active projects to develop tools for JML at present.

Contacts

  • The principal developer of OpenJML is David Cok: davidcok at users.sourceforge.net
  • 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:

  • 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
  • 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.
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.