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

language of guarded commands [7] that is close to actual code in general-purpose
programming languages.
In this paper we demonstrate the benefits of a link with Z that goes beyond
using pure JML. We do this: (i) by using a mechanical theorem prover to verify
some properties of a JML specification expressed in Z; and (ii) by pinpointing
the issues for the definition of a more systematic translation strategy between Z
and JML, and vice versa . The JML annotation syntax is divided into different
language levels; lower levels are mandatory, but higher levels are optional [24,
Sect. 2.9]. Starting from these lower levels, we concentrate on JML's specification
of abstract data types, leaving out other important aspects of JML annotations
as future work.
In [10], we formally specified in Z a hash map data type, an extension of the
work originally done in [11]. The Z hash map was used as a concrete refinement
for an abstract specification of the Unix filing system in [26]. We chose hash maps
because they provide constant-time performance for most operations, including
search and insertion. Although the Z hash map was tailored to the needs of the
filing system, we based it on the requirements from the Java documentation and
the JML specification. We took into account the essential properties hash maps
ought to have, such as strategies for resolving clashes of hash keys. The choice
for HashMap here remains an interesting proposition since it is widely used in
Java programs, and is among one of the most complex data structures within
the Java Collections Framework . 1
Some other classes have been subjected to this kind of scrutiny before. Huis-
man [17] has shown that the Java Set implementation (version 1 . 3) is not
guarded against Russell's paradox [31]). Earlier work verified the vector class
[15] and aspects of the JavaCard API [29,39]. Our translation is similar in spirit
to those between Z and BON/Eiffel [28] and BON and Object-Z [27].
2JMLSpifions
In this section, we give a brief overview of JML to help explain the HashMap spec-
ification. Suppose P , Q ,and R are boolean JML expressions ( i.e., Java expressions
with bounded quantifiers and mathematical sets), L is a list of locations ( i.e., ob-
ject attribute names, or an abstract collection of names), and E is some checked
Java Exception ( i.e., those exceptions that are part of a method signature).
The JML specification for a method m() is given as
/*@ assignable L;
@ requires P;
@ ensures Q;
@ signals (E) R; */
public void m() throws E { ... };
JML annotations are like Java comments but with an added “ @ ”sign.Apart
from the signals clause, this specification is like a specification statement in
1 See java.sun.com/docs/books/tutorial/collections .