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

MapOp
HashOp
idx < capacity
capacity = capacity
loadfactor = loadfactor

This states that the map parameters cannot change and that the current in-
dex being modified is within the map capacity, since we insist in no rehashing.
Operations also require a value ( val ?) with which to associate a key ( key ?):

ValMapOp =[ MapOp ; val ? , val !: VID ]

To associate a value with a key, we define the Put operation below. An Entry is
added into the map, hence it must be able to increase, and the current index is
the result of the hashing function on the given key ?.

Put
ValMapOp

idx = hf (( algo key ?) , capacity )
hm = hm

( idx , ( hm idx

⊕{ ( key ? , val ?) )) }

size = size +1

The effect is to update the map at the given index with the given ( key ? , val ?)
pair. This operation is more complex than it seems. There are at least three easy
cases to explain: (i) when key is not in any Entry in the map; (ii) when a key ?
with a consistent hash code and its mapping is being updated ( i.e., change of an
available mapping within an Entry ); and (iii) when a clash happens due to a key ?
that generates an inconsistent hash code, which leads to a “spiked” Entry in the
map. A further hidden complexity is about the injectivity of hm and its entries.
That creates an opportunity for general laws associating relational overriding (

)
for injective functions, as well as injective sequence concatenation ( ), where the
range of such a sequence has key-value pairs that are functional. This leads to
quite complex proof obligations and precondition calculation. As for Java, the
HM invariant on size should be relaxed to allow rehashing, so that clashes could
also happen whenever the map's capacity is exceeded.
The JML specification for the put method from the Map interface without
considering exceptional postconditions is given as

⊕

1 /*+@ public behavior
2 @ assignable objectState;

3 @ ensures (\exists Entry e; theMap.has(e); e != null

4 @ && JMLNullSafe.equals(e.abstractKey, key)

5 @ && JMLNullSafe.equals(e.abstractValue, value));

6 @ also
7 @+*/
8 /*@ public behavior