JML Home Page

About JML

The Java Modeling Language (JML) is a behavioral interface specification language 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.

The draft paper Design by Contract with JML (by Gary T. Leavens and Yoonsik Cheon) explains the most basic use of JML as a design by contract (DBC) language for Java.

The "white papers" below describe JML very briefly and some of its tools. The first of these gives a summary of all known tools. The second is a slightly dated summary of some of the main tools and how they relate to JML.

• Lilian Burdy, Yoonsik Cheon, David Cok, Michael Ernst, Joe Kiniry, Gary T. Leavens, K. Rustan M. Leino, and Erik Poll. An overview of JML tools and applications. International Journal on Software Tools for Technology Transfer, 7(3):212-232, June 2005. [preprint PDF] (The original publication is available at http://www.springerlink.com from http://dx.doi.org/10.1007/s10009-004-0167-4.)
• Gary T. Leavens, K. Rustan M. Leino, Erik Poll, Clyde Ruby, and Bart Jacobs. JML: notations and tools supporting detailed design in Java. In OOPSLA '00 Companion, Minneapolis, Minnesota, pp. 105-106. Copyright ACM, 2000. Also Department of Computer Science, Iowa State University, TR #00-15, August 2000. [abstract] [postscript] [PDF]

Tools

From the download page you can get a set of open-source tools for work with JML. The most useful of these are an assertion-checking compiler (jmlc), a unit testing tool (jmlunit), and an enhanced version of javadoc (jmldoc) that understands JML specifications. See the papers above and the documentation for details.

People

The work on JML is a cooperative effort between:

• Gary T. Leavens's JML group at the University of Central Florida (formerly at Iowa State University).
• The developers of the MultiJava project.
[an error occurred while processing this directive]

JML is an open project, and we welcome the participation of other groups. If your group is working on JML but not listed above, please send an email to Gary Leavens.

Development of JML is hosted on sourceforge.net.

Last modified Tuesday, January 8, 2008.