Last Modified:

These pages provide a quick introduction to JML (the Java Modeling Language) and OpenJML (a tool that checks specifications written in JML for Java programs) in the form of an on-line tutorial.

You should

  • read the brief What is Deductive Verification page to clearly understand the overall concept of deductive verification
  • follow the installation/execution/syntax instructions just enough to get you going
  • start with the Simple Method Specification sequence, but
  • branch out into other topics as you are interested
! This tutorial is a Work In Progress (March 2022).
! Expect lots of editing and new pages.

The tutorial does not cover all aspects of JML and OpenJML. See also the JML Reference Manual and the OpenJML User Guide.

Many tutorial pages have links to supplementary exercises. A table of contents for all the exercises is collected here.

Also note that there are additional standalone examples in a sibling page under Examples.

Tutorial Material All of the examples in this tutorial are part of the OpenJML installation zip file, in the top-level tutorial folder. For example, the T_ensures1 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 .out 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 openjml command.