Last Modified:

! These exercises are a Work In Progress (March-May 2022).
! Expect lots of editing, corrections and new material.

Supplementary Exercises for the JML Tutorial

Postconditions

Preconditions

Assert Statements

Assume Statements

JML Expressions

Well-Defined Expressions

Verifying Method Calls

Frame Conditions

Specifying Constructors

Using Method Calls in Specifications

Arithmetic

Visibility

Specifying Loops

Specifying Exceptions

Method Specifications

Multiple Method Behaviors