Information Technology Reference
In-Depth Information
key. Equality between elements of this given set is interpreted as Java structural
equality
(
o
1
∈
OID
∧
o
2
∈
OID
∧
o
1=
o
2)
⇔
o1.equals(o2)
Similarly, the given set
VID
is an abstract representation of object identifiers
that are mapped values, where we use the same interpretation of equality as
OID
.
These interpretations are important since the model field representing the array
of
Entry
in
HashMap
(
theMap
) is an instance of
JMLEqualsSet
(see Sects 2.1
and 2.3 above).
The schema
HashCode
represents the abstraction of the
hashCode()
algo-
rithm as an injection from the object instance (
OID
) to the corresponding hash
code value. It abstractly defines the behaviour of the
hashCode()
method in Z.
HashCode
HashAlgo
;
this
?:
OID
;
result
!:
Z
result
!=
algo this
?
From a given object instance
this
?, the hash code
result
! is output as the hash
value of the algorithm for that instance (
i.e., result
!=
this
?
.
hashCode()
). With
the abstract specification of
algo
as an injection, we can further refine it to
particular concrete implementations as needed, by coming back from generated
hash codes to the object instances that generated them.
Next, we model the underlying
Entry
for key-value pairs considering the clash-
ing mechanisms described above as
Entry
==
{
s
:iseq(
OID
×
VID
)
|
∀
o
:
OID
;
v
1
, v
2:
VID
|
o
→
v
1
∈
ran
s
∧
o
→
v
2
∈
ran
s
•
v
1=
v
2
}
Whenever two different object ids
o
1and
o
2 have the same normalised hash
code, a clash will happen and an entry may grow like in the example above.
In such cases, this “spiked”
Entry
specification enforces that: (i) no key-value
pairs are repeated in the list (iseq); and (ii) no clashes on different values can
happen for the same key object instance, the clashed pairs of
Entry
are func-
tional on the keys. The first property is defined in JML as an axiom, and we
have proved it as a trivial theorem based on our definition. In both cases, this
theorem/axiom is used to avoid a key being associated with different values.
The second property not only follows the
HashMap
contract, but it also enforces
that
Entry
keys properly implement
hashCode
by keeping hash keys immutable.
It also serves as a soundness invariant for the
hashCode()
of entries, whenever
they are values in other maps themselves. Also, the sequences
s
of
Entry
that
are entries represent ordering for clashes, where the injectivity (uniqueness) is
an optimisation for storage. This (uniqueness) restriction is indirectly enforced
in JML by the equational theory used in
theMap
model field. This model also
captures the eciency concerns for Java
HashMap
lifted from its JML specifi-
cation. As
Entry
is the most fundamental data structure to build a hash map,
Search WWH ::
Custom Search