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.
- 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.
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
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
- What is Deductive Verification
- Simple Method Specifications
- Assert statements
- Assume statements
- JML Expressions
- Well-defined Expressions
- Verifying Method Calls
- Frame Conditions
- Specifying Constructors
- Using Method Calls in Specifications
- Null and non-null
- 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
- 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