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

when badly programmed hash codes provide duplicates for different keys, and
so compromise the hash function. In both cases, Java's robust solution is to
have a linked list at the points of clash, so that in the worst case one gets a
“ spiked ” map, where the clashing entries grow outwards as linked lists. So, from
the previous insertion example, in the case of a clash with another value,

o1 != o2 && hf(o1.hashCode(), capacity) = hf(o2.hashCode(), capacity)

an update would become

map.put(o2, v2)

( hf ( o2.hashCode() , capacity ) → v1 , v2 )

Thus, a HashMap is like an injection from hash codes (generated by hf from
hashCode() considering the map capacity) into a sequence of abstractly defined
VALUE s, as roughly drafted in Z below

[ VALUE ]

“ HashMap == hf hashCode seq VALUE ”

We need to model in Z the Java hashing and clashing mechanisms described
above. We start defining the auxiliary structures that are the basis of a Z hash
map. This mechanised specification grew out of the original work done in [10,11],
and is slightly modified here for ease of presentation. Moreover, we assume maps
are neither keys nor values within other maps, as these would be special cases
(see Sect. 3.1). Nevertheless, they can be modularly handled later following some
Z specification patterns, as in [37].
A candidate hash function is trivially defined using integer division remainder,
bearing in mind the strictly positive capacity of the map involved.

hf : Z × N 1 → N

disabled rule dHashFcn

∀ hck : N 1 •

hf ( hck, n )= if ( hck

Z ; n :

≥ 0) then ( hck mod n ) else − ( hck mod n )

This provides separation of concerns, so that different implementations can pro-
vide more ecient hashing mechanisms without changing the clashing mecha-
nism and other mapping operations.
As most objects that are meant to be map keys have individual hashCode()
implementations, it is beside the point to specify them here. Instead, we abstract
hash code key generation below with the HashAlgo schema.

[ OID, VID ]

HashAlgo =[ algo : OID Z ]

We define the given set OID as an abstract representation of object identifiers
that are meant to be map keys. Those identifiers are either immutable objects or
do not structurally change ( i.e., keep the results of equals ) whilst being a map