Documentation
Language and Semantics
Documentation for JML is still in its early stages. 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.
-
Gary T. Leavens, Albert L. Baker, and Clyde Ruby.
Preliminary Design of JML:
A Behavioral Interface Specification Language for Java.
ACM SIGSOFT Software Engineering Notes, 31(3):1-38,
March 2006.
http://doi.acm.org/10.1145/1127878.1127884
Also Department of Computer Science, Iowa State University, TR #98-06-rev29, January 2006. [abstract] [postscript] [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] - 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), September 2009. [PDF] [postscript]
- 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 Wednesday, September 9, 2009.