These pages provide a quick introduction to JML (the Java Modeling Language) and OpenJML (a tool that implements checks of the specifications written in JML for Java programs) in the form of an on-line tutorial. Aside from the installation instructions, you can read the General pages as needed and dive right in to the section on Method Specifications.
Tutorial Material All of the examples in this tutorial are part of the installation
zip file, in the top-level
tutorial folder. For example, the
example is present as the
T_ensures1.java file. From within the tutorial
folder, you can run the example using
../openjml -esc T_ensures1.java.
Examples that produce output (e.g., error messages) have a corresponding
file containing the expected output.
The command-line to run the example is shown in the first line of the
example code; just add the appropriate path to the
- Simple Method Specifications
- Runtime Assertion Checking
- Advanced topics