Lecture 7: JML – the Java Modeling Language

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.


Most of the lecture was a walk-through of the main constructs of JML, which extend the simple Hoare logic significantly. I also discussed several of the tools available. The audience provided some astute questions, including how one might specify multi-threaded programs. I gave the short answer that this wasn’t easy and is a topic of current research; see below for a pointer.

You are strongly encouraged to try JML out by downloading one or more of the tools and trying the homework suggested at the end of the lecture note. It should be fun! See the next lecture for hints about using the ESC/Java2 tool.

References:

Edwin Rodríguez, Matthew B. Dwyer, Cormac Flanagan, John Hatcliff, Gary T. Leavens, Robby. Extending JML for Modular Specification and Verification of Multi-threaded Programs. ECOOP 2005: 551-576

A paper by Leavens and colleagues which proposes some extensions for JML to help specifying multi-threaded code.
These include phrases like locks this.lock and several more. This is delicate stuff; I’ll say more about it in some later lectures on concurrency.

Comments are closed.