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

Z State Schema and Initialisation. The state schema HM for Java HashMap
in Z is given below.

HM
hm : N → Entry ; HashAlgo

idx , size : N ; capacity , loadfactor : N 1

dom hm =0 ..capacity − 1

size ≤ capacity ∗ ( loadfactor div 100)

idx ∈ dom hm

∀ o : OID ; i : N | i ∈ dom hm • i = hf ( algo o, capacity )

It uniquely maps indexes into the entries array as the partial function hm ,where
all such indexes are valid within the map's capacity . Indexes are the result of
the hashing function ( hf ), which uses the object instance ( o )hashcoderesult
(from algo o ) modulo the initial capacity of the map. This establishes the link
between hash code indexes within the map ( i dom hm ), and object instances

( o )whose hashCode() algorithm we are interested in. The hm injection is rep-
resenting theMap JML model field in our Z model. It also represents the design
from the Map interface as an array of entries. Furthermore, idx defines the current
allocation position some mapping operations require. The loadfactor is useful to
balance the performance of the map for query, insertion, or iteration operations
adequately. In Java, loadfactor is given as a floating-point number supposed
to represent a percentage, but Z/Eves does not have floats. To accommodate
this, we normalise its value with integer division by 100, where the discrepancies
should be minor, since one usually uses whole integer percentages ( e.g., the de-
fault value is 75%). The few extra class invariants about capacity and loadfactor
that we have not mentioned already are given below.

∈

1 //@ public model int initialCapacity;
2
3 // loadFactor is spec_public below
4 //@ public invariant initialCapacity >= 0;
5 //@ public invariant loadFactor > 0;

We are puzzled by the JML invariant for initial capacity allowing zero capacity
maps. Although the Java documentation says that the capacity should be a
power of 2 (and zero certainly is), we think it is of little use to specify a map
that can never hold any element. Also, to avoid rehashing, we add an invariant
that the maximum size (or number of elements) the map can take is smaller
than the capacity multiplied by the (normalised) loadfactor .As size is loosely
defined, it follows the Java documentation suggestion that “if many mappings are
to be stored in a HashMap , creating it with a suciently large capacity will allow
the mappings to be stored more eciently than letting it perform automatic
rehashing as needed to grow”. Thus we changed the range of capacity in HM ,
and the relationship between size , capacity ,and loadfactor accordingly.
In JML, initialisation takes place at class constructors. In our case, we need
to consider the constructors for Object and HashMap ,as AbstractMap and the
implemented interfaces have no constructor specification. The default/implicit