Lecture 7: JML – the Java Modeling Language

2 February 2009

Review of Hoare logic.  Model-based specification as a technique for system design.  Design features of JML.  Some examples: preconditions, postconditions, invariants; model variables, methods and classes; ghost variables, assertions, assumptions.  JML as a common language across multiple tools for software specification and verification.

Read the rest of this entry »