A Formal Definition of JML in Coq

A Formal Definition of JML in Coq

and its Application to Runtime Assertion Checking

a Ph.D. Thesis presented by Hermann Lehner

Abstract

The Java Modeling Language (JML) is a very rich specification language for Java, which many applications use to describe the desired behavior of a program. The meaning of JML is described in a reference manual using natural language. The richness of JML, and the inherent ambiguity of natural language leads to many different interpretations of the same specification constructs in different applications.

We present a formalization of a large subset of JML in the theorem prover Coq. A formally defined semantics of JML provides an exact, unambiguous meaning for JML constructs. By formalizing the language in a theorem prover, we not only give a mathematically precise definition of the language but enable formal meta-reasoning about the language itself, its applications, and proposed extensions. Furthermore, the formalization can serve as JML front-end of a verification environment.

Frame conditions are expressed in JML by the assignable clause, which states the locations that can be updated by the method. For abstraction, the clause can mention dynamic data groups, which represent a set of heap locations. This set depends on the program state and may contain a large number of locations.

We present the first algorithm that checks assignable clauses in the presence of dynamic data groups. The algorithm performs very well on realistic and large data structures by lazily computing the set of locations in data groups and by caching already-computed results. We implemented the algorithm in OpenJML.

As an important contribution to runtime assertion checking, and as an interesting application of our formalization of JML in Coq, we proved in Coq that our algorithm behaves equivalently to the formalized JML semantics. This shows not only correctness and completeness of our algorithm to check assignable clauses, but also the usefulness and expressiveness of our JML formalization.