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

to the left-hand side of JML specifications line numbers, which are often re-
ferred to within the text. We also follow the convention to use arabic numerals
for the specifications copied from the JML distribution, and roman numerals for
specifications resulting from our experiments with Z.

2.3 Equational Theory

JML type system classes use an equational theory specified as a model method.
The equational theory for JMLEqualsSet specifies seventeen properties, which
are essentially some restricted forms or known set-theoretical laws [34, Chap. 4],
such as cardinality of empty sets ( S =

∅ ⇔

# S = 0) or set containment over

set union ( e S 2). We pay careful attention to this

equational theory for such JML sets since they are often used as model fields of
actual JML specifications, such as the one for HashMap .

∈ S 1 ∪ S 2 ⇔ e ∈ S 1 ∨ e ∈

1 //@ public model instance non_null JMLEqualsSet theMap;
2 //@

in objectState;

This model field (abstractly) represents the map as a set of Object instances
structurally equated with equals , which belongs to the data group of the general
Object state. By understanding how JML sets interpret equality, it is possible
to relate JML sets with the set-theoretical data types and notion of equality in
Z, as shown below for Z hash maps (see Sect. 3).

2.4 Nullability and Instance Cloning

Another concern within JML is the “nullability” of method parameters and
results, and object attribute initialisations. The JML type system provides fa-
cilities to handle null objects so that equality tests on sets (and other data
structures) containing null objects are well defined and do not throw excep-
tions, such as in the JMLNullSafe class. We assume in this paper that no hash
key or associated value within the Z hash map will ever be null . The effect of
relaxing this assumption is a more verbose and laborious specification, without
much insight or novelty added. Thus, we have traded the treatment of null for
the investigation of additional properties of hash maps and automation mecha-
nisation rules, as present in Sect. 3.4.
JML addresses object cloning via the specification of the clone() method for
the Object class. It specifies how cloned object instances preserve the original
class type, general (attribute) structure, and produce no side effects. In Java,
only objects that implement the Cloneable interface can be cloned. In general,
for any Object that implements the Cloneable interface, clone() is side-effect
free, and has a non-null result of the same dynamic type as the cloned object.

1 /*@ protected normal_behavior
2

@ requires this instanceof Cloneable;

3 @ assignable \nothing;

4 @ ensures \result != null && \typeof(\result) == \typeof(this);

5 @ ensures (* \result is a clone of this *);

6 @*/