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

constructor from Object is trivial. Like a Ξ schema in Z, it just states no at-
tributes are modified.

1 /*@ public normal_behavior
2

@ assignable \nothing;

3 @*/
4 public /*@ pure @*/ Object();

HashMap has various constructors, which could all be related to one single version
that we transcribe below.

1 /*@ public normal_behavior
2 @ requires initialCapacity >= 0;

3 @ assignable theMap, this.initialCapacity, this.loadFactor;

4 @ ensures theMap != null && theMap.isEmpty();

5 @ ensures this.initialCapacity == initialCapacity

6 @ && this.loadFactor == loadFactor;

7 @*/
8 public HashMap(int initialCapacity, float loadFactor);

It just initialises the capacity and loadfactor , and guarantees that theMap model
field is non-null and empty. For the Z state schema, initialisation is also trivial,
but slightly different.

InitHM
HM ; c ? , l ?: N 1

algo hm =

= ∅ ∧ ∅

capacity = c ? ∧ loadfactor = l ?

size = idx =0

We must also ensure that there is always an algorithm to go from an OID to its
corresponding hashCode() ( i.e., algo ), which is trivially true ,since algo is

total, and we can assume OID to be a non-empty type.

= ∅

3.2 Map Operations

Now we can define the map operations in Z from the JML specification of
HashMap methods. We define some useful schemas shared among the operations.

HashOp

=[ ΔHM ; key ?: OID ; result !:

Z | HashCode [ key ? /this ?] ]

KeyQueryOp =( HashOp ∧ Ξ HM )

ValQueryOp =[ Ξ HM ; val ?: VID ]

The HashOp schema represents all operations involving hash keys ( key ?), where
the resulting hashCode() value is calculated via the HashCode schema, and is
output in result !. Query ( Ξ ) operations in Z are those that do not change the
state. We define one for keys ( KeyQueryOp ) and one for values ( ValQueryOp ),