Information Technology Reference
In-Depth Information
where the former requires a key and produces a hash code, whereas the latter
requires an object identifier for mapped values ( val ?). This reuse via schema
inclusion is useful in simplifying proofs from unrelated predicates, and it keeps
the specification modular.
Next, we specify HashMap containment queries for keys and values within the
map. Key containment is a query operation that ascertains that there exists an
entry in theMap model field such that the given key is structurally equivalent to
the given key. This operation is specified in the Map interface as
1 /*+@ public normal_behavior
2
@
ensures \result <==>
3
@
(\exists Map.Entry e; theMap.has(e) && e != null;
4
@
JMLNullSafe.equals(e.abstractKey, key));
5 @+*/
6 /*@ pure @*/ boolean containsKey(/*@ nullable @*/ Object key);
The Z equivalent is a bit different from the JML version. Instead of having an
existential postcondition being equivalent to a boolean value ( i.e., a false result
could still be a true postcondition), it explicitly mentions the key containment
condition within the hash map. We make sure this difference is harmless by
proving the ensures clause above as a theorem in Sect. 3.4. The next schema
specifies the hash key containment query operation.
ContainsKey
=[ KeyQueryOp
|
key ?
dom (ran ( hm idx )) ]
It has the signature of KeyQueryOp , where the input key ? is within the ap-
propriate projection in theMap (represented by hm ). The universally quantified
invariant in HM allows us to link hash map (array) indexes ( idx ), in this case
calculated from key ?, with the hash code algorithm ( algo ), in this case stored
in result !. When we apply idx to hm ,wegetan Entry , which is an injective
sequence where the range is ( OID
VID ) pairs. From these pairs, we check
whether the given key ? is present in the map or not using dom. The JML speci-
fication for value containment is very similar, and we omit it here. The Z schema
is also very similar and is given below.
×
ContainsValue
ValQueryOp
val ? ran (ran ( hm idx ))
The same principle applies, but now we are interested in projecting the values
( val ?) from the ( OID
×
VID ) pairs from the Entry at idx in hm . Thus, we just
use ran instead of dom.
The emptiness operation does not produce side effects and relates the hash
map array hm with size .Ifthearrayisempty,then size must be zero. Yet if
the size is zero, the Java documentation does not insist the array should be
initialised as empty.
IsMapEmpty
=[ ΞHM
|
hm =
size =0]
 
Search WWH ::




Custom Search