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

we see the finding and interpretation of such invariants as very useful. But they
didn't appear by magic: they were discovered by using the theorem prover in
the refutatory style advocated in the classical style [23, p.127], in order to reach
an elegant specification that is amenable for mechanisation.
The JML axiom about the functionality of entries is given in the specification
of the Map interface that HashMap implements in terms of the contains model
methods, as transcribed below

1 /*@ public normal_behavior
3 @ requires e != null;
4 @ ensures \result <==> contains(e.getKey(),e.getValue());
5 @ public pure model boolean contains(Entry e);
7@
8 @ public pure model boolean contains(Object key, Object value);
9@
10 @ axiom (\forall Map m; (\forall Object k, v, vv;

11 @ (m.contains(k,v) && m.contains(k,vv)) ==>

12 @ JMLNullSafe.equals(v,vv)));

13 @*/

The model method in line (8) is important since its use is propagated throughout
most of the HashMap specification. Despite this fact, it has no explicit specifica-
tion, which means it has just the trivial postcondition true , whatever the given
Entry .As theMap model field used to represent the array of entries implements
an equational theory for structural equality ( i.e., JMLEqualsSet ), we were sur-
prised it was not linked with contains . This link was hinted at as one of the class
invariant examples mentioned earlier (see Sect. 2.5), since the has() method is
defined in terms of the right equational theory.

1 /*+@ public instance invariant
2 @ (\forall Object o1, o2; theMap.has(o1) && theMap.has(o2);

3 @ o2!=o1 ==> !JMLNullSafe.equals(o2,o1));

4 @*/

We are not certain if this would enforce the right specification for containment.
We suggest to explicitly add a link between theMap and contains ,as

i /*@ public normal_behavior
ii @ requires e != null;
iii @ ensures \result <==> theMap.has(e) ;
iv @ public pure model boolean contains(Entry e);
v@
vi @ public normal_behaviour

vii @ requires key != null && value != null;

viii @ ensures \result <==> contains(e.getKey(), e.getValue());

ix @ public pure model boolean contains(Object key, Object value);

x @*/

For JML, the restriction on non-null key/value could be relaxed or generalised
to handle null .