Proving Theorems About JML Classes - Formal Methods and Hybrid Real-Time Systems - page 255

Proving Theorems About JML Classes

Leo Freitas and Jim Woodcock

Department of Computer Science
University of York, UK
{ leo,jim } @cs.york.ac.uk

Abstract. We present an initial link between Z and JML that has en-
abled us to use Z/Eves to prove theorems about JML classes. We have
applied this to the JML type system and the Java HashMap class from the
Java Collections Framework . We present and discuss the issues behind a
more general strategy for translation in both directions between Z and
JML. This work is a contribution to the Verified Software Repository ,
part of the Grand Challenge in Verified Software .
Keywords: Grand Challenge in Verified Software, JML, Java Collec-
tions Framework, Java HashMap class, Java Modeling Language, formal
specification, linking theories, mechanical theorem proving, software ver-
ification, Verified Software Repository, Z, Z/Eves.

On the occasion of the 70th birthdays of Dines Bjørner and Zhou Chaochen.

1 On Linking Z and JML

The Java Modeling Language (JML) [3] is a language used to specify more
clearly than informal documentation the behaviour of Java programs [12] by
using annotations as Java comments. These annotations not only document the
code, but also enable static checking, run-time assertion checking, and other
verification tasks to be performed on the target code, such as loop invariant
detection [16,4]. The JML toolset contains a number of other tools, such as an
annotation parser and typechecker, an HTML ( JavaDOC -style) documentation
generator for JML annotations, an automatic unit test set generator, and so on.
In various syntactic forms, JML annotations are predicates specifying declara-
tive behaviour, such as pre- and postconditions, class and instance invariants,
modifiable-variable frames, concurrent andreal-timebehaviour, resource alloca-
tion in terms of memory and computational time, and so on [24]. JML supports
a lightweight style of specification, where annotations start as quite trivial pred-
icates, and are then enriched over time by adding extra constraints.
The Z notation [34] is a formal specification method that has enjoyed a cer-
tain acceptance amongst academic and industrial practitioners for more than
two decades [36,42,18], and was standardised by ISO in 2002 [20]. Z is useful for
specifying abstract data types and their corresponding operations, as well as for
proving data refinement from an abstract specification to a concrete implemen-
tation [41], at which point a refinement calculus [1,25,6] can be used to reach a