The Java Modeling Language (JML)

Documentation

Language and Semantics

The main documentation for JML is currently the Reference Manual:

• David R. Cok, Gary T. Leavens, and Mattias Ulbrich. JML Reference Manual (Second Edition, PDF).
• Gary T. Leavens, Erik Poll, Curtis Clifton, Yoonsik Cheon, Clyde Ruby, David Cok, Peter Müller, Joseph Kiniry, Patrice Chalin, and Daniel M. Zimmerman. JML Reference Manual (DRAFT), May, 2013. [PDF] [postscript]

The following include tutorial examples and papers that describe JML itself.

• Gary T. Leavens, Yoonsik Cheon. Design by Contract with JML. (Draft tutorial for JML in PDF format)
• Gary T. Leavens, Albert L. Baker, and Clyde Ruby. JML: A Notation for Detailed Design [postscript] [PDF]. In Haim Kilov, Bernhard Rumpe, and Ian Simmonds (editors), Behavioral Specifications of Businesses and Systems, chapter 12, pages 175-188. Copyright Kluwer, 1999. Used by permission.
• Preliminary design of JML: a behavioral interface specification language for Java

  Gary T. Leavens, Albert L. Baker, Clyde Ruby
  ACM SIGSOFT Software Engineering Notes, 31(3):1-38, March 2006.
  
  The published verison has a mistake, figure 12 repeats figure 11. A corrected version is found in prelimdesign.pdf.
• Patrice Chalin, Joseph R. Kiniry, Gary T. Leavens, and Erik Poll. Beyond Assertions: Advanced Specification and Verification with JML and ESC/Java2. In Formal Methods for Components and Objects (FMCO) 2005, Revised Lectures, pages 342-363. Volume 4111 of Lecture Notes in Computer Science, Springer Verlag, 2006.
  The original publication is available at springerlink.com or directly from http://dx.doi.org/10.1007/11804192_16.
  [Corrected PDF]
• Arun D. Raghavan and Gary T. Leavens. Desugaring JML Method Specifications. Department of Computer Science, Iowa State University, TR #00-03e, March 2000, revised July, December 2000, August 2001, July 2003, May 2005. [abstract] [postscript] [PDF]

See also the papers page for more detailed studies of JML's semantics.

Tool Documentation

Common JML Tools Manual Pages

The following are unix-style manual pages for each of the tools in the Common JML tools Release. This documentation is also available in the JML.html file in the release. The manual pages each have some information on how to use the tool, and specify their options and arguments.

• jml-launcher (the launcher for the graphical user interface tools).
• jml and jml-gui (the checker).
• jmlc and jmlc-gui (compile for runtime assertion checking).
• jmldoc and jmldoc-gui (a version of javadoc that includes JML specification information).
• jmle (compile for executing or prototyping specifications).
• jmlrac (a version of Java, the VM, that includes the bin/jmlruntime.jar file in the CLASSPATH, for running files compiled with jmlc).
• jmlre (a version of Java, the VM, that includes the runtime support needed for executing specifications, for running files compiled with jmle).
• jmlspec and jmlspec-gui (generate skeleton specification files from Java source files).
• jmlunit and jmlunit-gui (produce unit testing code stubs for use with JUnit).
• jtest (combines the work of jmlc and jmlunit)
• jml-junit (a version of JUnit's swing user interface that includes the bin/jmlruntime.jar and bin/jmljunitruntime.jar files in the CLASSPATH, for running JML and JUnit based tests on files compiled with jmlc and test cases generated by jmlunit).

Last modified Tuesday, December 14, 2021.