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

8 @ public code normal_behavior

9 @ assignable \nothing;

10 @+*/
11 public int hashCode();
This is a loose specification that permits the hash code calculation to have
“benevolent side effects” on the objectState model field, and should rely on the
hashValue() model method (see Sect. 2.2). The ensures clause (line (4)) is sim-
ply informal text, as meta-comments just evaluate to true. Although it not quite
clear what it means for side effects to be “benevolent”, one could argue that they
would be related to unobservable by external clients, such as caching schemes. It
is also not quite clear what the motivations were for not enforcing in the postcon-
dition the invariant (line (5)) as defined by the hashValue() model method (see
Sect. 2.2). There are two problems with this under-specification: (i) hashCode is
not side-effect free, since the second behaviour (lines (7-10)) has no postcondi-
tion; and (ii) even if one agrees that there is a case for “benevolent side effects”,
nothing is given to enforce the invariant between hashCode and equals (see
Sect. 2.1). Perhaps, this choice is based on some undisclosed technicality, or is
still under development. We think a more intuitive specification would be:

i /*@ public behavior
ii @ assignable \nothing;

iii @ ensures (* \result is a hash code for this object *);

iv @ ensures \result == hashValue();

v @*/
vi /*@ pure @*/ public int hashCode();
As the map implementation is modelled as an array of Entry , its hash code
specification is also important. Despite this fact, there is no JML specification
for it. The Java documentation says that provided the key-value is not null
(which in our case we assume to always be true ), then the hash code of an
Entry e is the bitwise exclusive or ( xor ) integer operator between the hashCode
of key and value (lines (v-vi)). So, a candidate JML specification would be

i /*@ also
ii @ public normal_behaviour

iii @ assignable \nothing;

iv @ requires getKey() != null && getValue() != null;

v @ ensures (\result == getKey().hashValue() ^

vi @ getValue().hashValue());

vii @*/
viii /*@ pure @*/ public int hashCode();

We inherit the specification from Object with also (line (i)), and add the ex-
pected side-effect free (in line (iii)) postcondition (line (v)), provided the Entry
has non-null elements (line (iv)). This keeps the equals / hashCode invariant
among any Entry within the map implementation. If hashCode was specified as
pure in Object , we could have used getKey().hashCode() instead.

Handling Clashes. Clashes can happen either when there are more entries
than room available, in which case the map could expand (and be rehashed), or