Documentation
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, and Joseph Kiniry. JML Reference Manual (DRAFT), October 2007. [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.
Last modified Tuesday, January 8, 2008.