A JML tutorial: Modular specification and verification of functional behavior for java

Abstract

JML, the Java Modeling Language, is the lingua franca of researchers working on specification and verification techniques and tools for Java. There are over 23 research groups worldwide working on various aspects of the JML project. These groups have built a large suite of tools for automated checking and verification (see http://jmlapecs.org). This tutorial will present JML features useful for specifying the functional behavior of sequential Java classes and interfaces. Participants will get hands-on experience writing JML specifications for data types, including pre- and postconditions, frames, invariants, history constraints, ghost and model fields, and specfication inheritance. They will also see how to verify object-oriented code using supertype abstraction for modular Hoare-style reasoning. Finally there will be an exchange of ideas on improving existing JML tools, open research problems, and future directions for research related to JML, including ways to connect JML to various theorem provers. © Springer-Verlag Berlin Heidelberg 2007.