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 papers below describe JML very briefly and some of its tools. The paper Beyond Assertions: Advanced Specification and Verification with JML and ESC/Java2 (by Patrice Chalin, Joseph R. Kiniry, Gary T. Leavens, and Erik Poll) contains a description of JML and its tools that is suitable for those who are already more familiar with the idea of assertions. The second gives a summary of all known tools.


From the download page you can choose between several open-source tools for using 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.


The work on JML is a cooperative effort between:

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 Logo

We have yearly workshops on JML. The 2017 workshop on JML is hosted at UCF by Gary Leavens.

Last modified Thursday, December 14, 2017.