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

identity ( == ) equality (named JMLObjectSet ), or structural ( equals ) equality
(named JMLEqualsSet ); and mathematical sets of JMLType elements compared
with structural equality (named JMLValueSet ). The collection of objects uses
aliasing for the elements, whereas the mathematical set uses cloned (shallow
copied) versions of the elements. The JMLValueSet classisusedasaJMLmeta-
specification for extending JML's type system, whereas the JMLEqualsSet and
JMLObjectSet are aimed at JML specifications from practical users, where the
same applies for other mathematical entities like sequences and bags. These in-
ternal JML classes also contain JML annotations. As the JML annotated version
of Java HashMap uses JMLEqualsSet , we give some more detail on it in Sect. 2.
A final concern when implementing equals is its relationship with the Java
“ int hashCode() ” method, which provides a unique hash code for object in-
stances. The Java documentation states that structurally equivalent objects must
have the same hash code.

o1 . equals ( o2 )

⇒ o1 . hashCode () = o2 . hashCode ()

The reverse is not required, but is desirable since it improves the performance of
HashMap implementations. Ideal implementations of these two methods are avail-
able for the unaware programmer, such as the EqualsBuilder and HashCode -
Builder classes of the Jakarta Commons Apache library, 2

which provide

adequate solutions as suggested in [2].

2.2 Abstraction Mechanisms
JML allows specification abstraction through the definition of model fields and
methods. These are specification devices that exist only as JML annotations and
do not have a direct counterpart in Java code, but can be used as part of the
annotations specifying concrete Java methods. For instance, the Object class
specification has one model field representing the (abstract) object state

1 //@ public model non_null JMLDataGroup objectState;
This model field is a placeholder to represent whatever attributes derived classes
might have. A JMLDataGroup is an abstraction device representing a set of lo-
cations that can appear in assignable clauses. Data groups are particularly
useful in allowing different visibilities among model fields: it is possible to state
that private and protected instance fields used to compute public model fields
are assignable .The Object class also has an example of a model method that
raises our interest

1 // The value produced by hashCode() but without any side effects.
2 //@ ensures (\forall Object o; this.equals(o)
3 // ==> \result == o.hashValue());
4 //@ public pure model int hashValue();
The hashValue() model method is a side-effect free version of the hashCode()
method that obeys the Java documentation requirement that structurally equiv-
alent objects must have the same hash code. For clarity of presentation, we add

2 See jakarta.apache.org/commons .