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

The normal behaviour keyword is for exception-free postconditions. Cloned
arrays must preserve all elements: all cloned array elements have the same object
identity, and clone is specified as a shallow copy.

7 /*@ ...
8 @ requires this.getClass().isArray();

9 @ ensures (\forall int i; 0 <= i && i < ((Object[])this).length;

10 @ ((Object[])\result )[i] == ((Object[])this)[i]);

11 @*/
12 protected /*@non_null*/ Object clone() throws ...;
A similar specification is added for other primitive array types. As Object itself
does not implement Cloneable , this specification lays the foundation but cannot
be used yet. Derived classes that implement Cloneable usually add a further
(standard) postcondition, like the one below for HashMap , which strengthens
dynamic typechecking (line (4)), guarantees structural equality (but not object
equality) with this (line (5)), and is side-effect free (line (3)).

1 /*@ also
2 @ public normal_behavior

3 @ assignable \nothing;

4 @ ensures \result instanceof Map && \fresh(\result)

5 @ && ((Map)\result).equals(this);

6 @ ensures_redundantly \result != this;

7 @*/
8 public Object clone();

The also keyword conjoins this specification for HashMap with the one inherited
from Object .The ensures redundantly clause (line (6)) states a direct conse-
quence of the previous postcondition that is useful for automatic tools that might
not be able to deduce this directly. As object cloning is a low-level implemen-
tation issue, it does not quite have a direct correspondence in a Z specification,
unless one is concerned with memory management. As our focus is to investigate
the HashMap functionality, we do not consider cloning any further.

2.5 JML Invariants

JML also provides instance or class ( static ) invariants. These are predicates
that always hold for visible object states [24, Sect. 8.2]. In JML's terminology [24,
p. 50-51], invariants can be assumed , established ,or preserved .Foreachmethod
and constructor, class invariants can be assumed by the class type at visible pre-
states and are established at visible post-states. Instance invariants are similar.
Invariants that are both assumed and established are preserved.
For instance, Java models HashMap as an array of Entry objects as key-value
pairs, where the following instance invariants about type consistency among
Entry in theMap model field holds.

1 // only standard JML tools understand *+@ annotations
2 /*+@ public instance invariant
3

@ (\forall Object o; theMap.has(o); o instanceof Map.Entry);