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

They specify that on the assumption of an initialised (instantiated) map ( HM )
and an appropriate key ?/ val ?, the JML (postcondition) specification of the corre-
sponding boolean operation holds, provided there exists a counterpart identifier
within the map at a known Entrye index.

3.4 Theorems and Automation Rules

In order to make sure our Z specification indeed meets the expected JML post-
conditions, we prove their ensures clauses as Z theorems. The JML ensures
clause for the containsKey method is
1 @ ensures \result <==>
2 @ (\exists Map.Entry e; theMap.has(e) && e != null;
3 @ JMLNullSafe.equals(e.abstractKey, key));
where the Z theorem showing that it holds is given next.

theorem tContainsKeyEnsures
∀ ContainsKey •∃ val : VID • ( key ? , val ) ∈ ran ( hm idx )

That is, if the ContainsKey operation is successful, then that means there must
exist some value val for which the contained key ? is within the map hm at the
index idx calculated via algo in HM . Similarly, the JML specification for the
get method postcondition is
1 @ ensures (\exists Entry e; theMap.has(e); e != null
2 @ && JMLNullSafe.equals(e.abstractKey, key)
3 @ && \result.equals(e.abstractValue));
where the Z theorem ensuring that for the given key ?, the result ( val !) is indeed
a mapping within the map ( hm )isgivenas.

theorem tGetValueEnsures
∀ GetValue • ( key ? , val !) ∈ ran ( hm idx )

One can carry on doing this for the other operations until the complete set of
ensures clauses have been proved. For class invariants that have not already
been given as definitions, we would need to prove a theorem for every operation,
where we could assume the operation and we needed to show that the invari-
ant holds. Fortunately, as the Map axiom about functionality of key-value pairs
is given in the definition of Entry , and the other class invariants are related
to equality and type consistency, we have proved all the theorems about map
instance invariants.
The successful mechanisation of a JML-inspired Z hash map heavily depends
on a good set of automation rules that are tailor-made to the complexity of the
data structure being manipulated, in this case an injective map of Entry .For
instance, the maximal type of hm

∈ N Entry is as follows

hm ∈ P Z × P Z ×

( OID

× VID )))

( (

During proofs, it often happens that one gets different versions of this type as
proof obligations, such as