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

4 @*/
5 /*+@ public instance invariant
6 @ (\forall Object o1, o2; theMap.has(o1) && theMap.has(o2);

7 @ o2!=o1 ==> !JMLNullSafe.equals(o2,o1));

8 @*/

It specifies that theMap elements are a subtype of Entry (lines (2-4)), and that
different Entry elements (by object identity) within theMap cannot be struc-
turally equivalent (lines (5-8)), bearing in mind the treatment of equality among
null objects through the JMLNullSafe class. As the specification of equals for
Entry below relies on the implementation of equals for the key and the value,
this second class invariant is more interesting: it enforces that key-value pairs
within different entries properly implement their structural equivalence algo-
rithm (in lines (4-6) below); and that they are side-effect free (with pure keyword
in line (9)); the keyword pure is an abbreviation for assignable \nothing .

1 /*+@ also
2

@ public normal_behavior

3 @ requires o instanceof Entry;

4 @ ensures \result ==

5 @ (JMLNullSafe.equals(((Entry)o).abstractKey, abstractKey)

6 @ && JMLNullSafe.equals(((Entry)o).abstractValue,

7 @ abstractValue) );

8 @+*/
9 /*@ pure @*/ public boolean equals(/*@ nullable @*/ Object o);

The specification for equality between map entries relies on the structural equal-
ity of the array of Entry as the key-value pairs it represents. This care with
structural equality is needed since the equational theory used in the JML spec-
ification of theMap model field is the one from the JMLEqualsSet class. JML
also allows the declaration of class axioms. The JML tools within the standard
distribution usually ignore these axioms [3], but theorem provers within some
more powerful JML tools [16,4] assume them as lemmas.

3 Formalising Java HashMap sinZ

With this basic introduction to JML, we start linking the JML specification of
Java's HashMap with an extended Z hash map from [8,11]. The JML specification
for HashMap encompasses the specifications of its inheritance tree: the Object ,
AbstractMap ,and HashMap classes; and the Map , Cloneable ,and Serializable
interfaces. As mentioned above, we are not interested for now in object cloning or
serialisation, and hence we concentrate on the other classes and interfaces. We are
also not concerned here with specification for nullability or exception handling,
and hence we omit them. Some of the JML specifications for Object and Map were
already introduced in the previous section.TheotherJMLelementsweconsider
are detailed below together with their corresponding Z counterparts. They are
the invariants, assignable variables, method preconditions, and exception-free
method postconditions ( i.e., ensures rather than signals clauses).