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