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

In presenting the Z material, we follow the bottom-up style of the Z/Eves the-
orem prover [32] that we use to define the Z hash map. All material presented
here has been mechanically verified, and the conjectures proved as theorems.
We point out opportunities for completing the JML annotations, either with
theorems developed in Z, or directly with definitions drawn from the Java docu-
mentation. These are merely suggestions, since we have not yet established how
to formally link Z and JML (see discussion in Sect. 4), but we find them useful.

3.1 Java HashMap Design in Z

In Java, a HashMap represents Object keys mapped to Object values, where
the key's hashCode() method is used to uniquely index entries of key-value
pairs into an underlying array-like data structure. This array of Entry objects
within the map is functional ( i.e., Key Value ). The map has two parameters

allowing trade-off between operations performance: an initial capacity and a load
factor. The capacity is the length of the array of entries, whereas the load factor
measures how full the map may get before its capacity is automatically increased.
This design provides constant-time performance for basic query and insert op-
erations, assuming the hash function disperses the elements properly. Iteration
over the map requires time proportional to the capacity (the initial array size),
plus the number of actual key-value pairs. When the number of map entries
exceeds the product of these parameters, the array is rehashed to allow room
for further entries. In this way, these two parameters can be used to trade-off
performance between get/put and iteration operations. As Object instances are
given as map keys, care must be taken if their structure (the result of their
equals method) could change whilst within the map. Map keys are not im-
mutable and may suffer from side effects, in which case the behaviour of the
map is not specified. Thus, maps themselves should never be keys, and if they
are values in Entry ,the equals and hashCode methods of the map would no
longer be well-defined.

→

Hash Code Values. The hash code integer ( Z )fromamapkey( o1 )isnor-

malised to a strictly positive integer ( N 1 ) via a hashing function ( hf ), taking

into account the map's capacity.

i.e., map.put(o1, v1) ( hf ( o1.hashCode() , capacity ) → v1 )

As map keys are Object instances, we need to consider the Object JML speci-
fication for hashCode()

1 // for subclasses with benevolent side effects
2 /*@ public behavior
3 @ assignable objectState;
4 @ ensures (* \result is a hash code for this object *);
5 @ //ensures \result == hashValue();
6 @*/
7 /*+@ also