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

Table 1. Operations precondition table

InitHM ( ∃ m : N Entry ; a : OID Z ; c ?: N 1

• dom m =0 ..c ? − 1 ∧ a = ∅
∧ ( ∀ o : OID ; i :dom m •
i = hf (( ao ) , c ?)) )

ContainsKey key ? ∈ dom (ran ( hm idx ))

ContainsValue val ? ∈ ran (ran ( hm idx ))

IsEmpty true

GetValue pre ContainsKey

Put size < capacity ∗ ( loadfactor div 100)

( m ) instantiated with enough room for the given (strictly positive) capacity ( c ?),
as well as a valid hashCode() algorithm ( a = ∅ ) mapping object instances ( o )

spread across the HashMap array indexes ( i dom m ). The strictly positive ca-

pacity and hashCode() algorithm availability are trivially true in practice, since
a boundary check ( c ?

∈

1) is made at instantiation time, and all Java Object
instances have a default hashCode() implementation as their (unique) object
address in memory. Nevertheless, this default value might not always be the
best one from an implementation point of view, as hashCode() implementations
ought to be consistent with respect to equals . It is also nice to confirm that
the precondition for GetValue was indeed what the JML requires clause says
it is: the precondition for ContainsKey .
Not surprisingly, the most complex proof was the one for the Put operation.
That is because there are far too many cases to consider: when the key is within
the map or when it is a new one; when clashes happen; and so on. Also, relational
overriding and sequence concatenation over injections require a great deal of
machinery and ingenuity in order to finish the proof. Thanks to previous work
done for a similar operation on injections in Mondex [42], the work here was
considerably reduced. That is both because of general proof strategies that have
been reused, and because additional Z toolkit laws for injections and injective
sequences were added. This is positive and encouraging evidence of what can be
generally achieved with the pilot project verification experiments, and verified
components: reusable toolkit laws and proof strategies.
As the JML specifications for the boolean operations were given as existen-
tially quantified postconditions over a key-value pair in an Entry within the
map, we decided to prove additional theorems to show that such a specification
is as good as the one we found. This is defined in the next two theorems

≥

theorem tContainsKeyPRE2
∀ HM ; key ?: OID | ( ∃ val : VID • ( key ? , val ) ∈ ran ( hm idx )) •

pre ContainsKey

theorem tContainsValuePRE2
∀ HM ; val ?: FILE | ( ∃ key : OID • ( key, val ?) ∈ ran ( hm idx )) •

pre ContainsValue