Teaching Material for JML
The following is mostly for teaching JML to programmers or students in a course in a University. Contributions are welcome. If you are a developer on the sourceforge.net jmlspecs project, you can update the CVS for this web page by checking out the module named web and commiting changes to the teaching.shtml file. Or, if you aren't a developer, please send some XHTML we can use to link to your materials to Gary Leavens.
-
The following are some materials from the JML web pages that may be
helpful.
- See the main JML web page for overview and white papers that describe JML and its tools.
- Gary T. Leavens, Yoonsik Cheon. Design by Contract with JML. (Draft tutorial for JML in PDF format)
- See the JML documentation page for reference material, including the preliminary design document, which is more like a short reference manual.
- See the examples page for various instructive examples of JML. In particular look at the samples (which are also included in the directory JML/org/jmlspecs/samples of the JML release). In particular, look at the package org.jmlspecs.samples.dbc for examples in the design-by-contract style that is most suitable for teaching students about JML (and is also compatible with ESC/Java).
- Yoonsik Cheon has some power-point slides introducing JML and design by contract using JML.
-
Gary T. Leavens,
Joseph R. Kiniry, and
Erik Poll
wrote a tutorial on JML, which Gary gave at CAV 2007 on July 3, 2007.
You can get the following:
- Slides with notes, suitable for reading by yourself.
- Slides only (no notes), suitable for actual presentation.
- Handouts, printed slides, without any of the answers, suitable for passing out as handouts.
- A zip file with the sources, in LaTeX beamer format, including all the examples. These sources are also available in the ESCTools project, under the "slides" directory.
- A directory of the sources for the examples used in the tutorial (mostly JML, but beware that there are some errors that are intentional, especially in the Java code).
- Gary T. Leavens has material on "Design with JML" from his course in object-oriented analysis and design. Look in the file Outline-files.txt for a list of the other lecture notes to look at, and the order in which they are to be taught (junit.txt, jml.txt, and jml-junit.txt). See his README.txt for some explanation of the notation. There is also a related homework and the HistoricalData.java file used in the homework.
- Simanta Mitra has made a lab exercise based on JML and JUnit for his course on testing.
- Gary T. Leavens ran a JML Seminar at Iowa State in Fall 2005. There are some homeworks available.
- Gary T. Leavens is running a reading seminar on Specification and Verification for Java-like languages at Iowa State in Spring 2007.
- Gary T. Leavens has power-point slides for a talk on JML, including supertype abstraction, specification inheritance and behavioral subtyping.
- The Lecture notes on Formal Methods in the Software Life Cycle by Erik de Vink from the University of Eindhoven, and Engelbert Hubbers, Martijn Oostdijk, and Erik Poll from the University in Nijmegen contains some material on JML (in English).
Last modified Friday, August 10, 2007.