JML Tutorial
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.
- What is Deductive Verification
- Simple Method Specifications
- Postconditions
- Preconditions
- Assert statements
- Assume statements
- JML Expressions
- Well-defined Expressions
- Verifying Method Calls
- Frame Conditions
- Specifying Constructors
- Using Method Calls in Specifications
- Arithmetic
- Null and non-null
- Visibility
- Specifying Loops
- Specifying Exceptions
- Method Specifications: old clauses and clause ordering
- Multiple Method Behaviors
- Minimizing replicated specifications — initially, constraint, invariant clauses
- Ghost variables and computations
- Inheritance
- Built-in mathematical types for specifications
- Managing proofs
- Debugging Techniques
- Runtime Assertion Checking
- Advanced topics
- Specification (.jml) files
- Java @-annotations for JML
- Reasoning about bit-wise operations
- Reasoning about Floating Point operations
- Reasoning about Enums
- Reasoning about Records
- Reasoning about Lambda Functions
- Reasoning about Streams
- Reasoning about Types
- Reasoning about locks
- Reasoning about recursive functions and data structures
- Reasoning about non-deterministic functions and volatile variables
- Reasoning about termination