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

9 @ assignable objectState;

10 @ ensures (\exists Entry e; contains(e);

11 @ nullequals(e.abstractKey, key)

12 @ && nullequals(e.abstractValue, value));

13 @ ensures (\forall Entry e; \old(contains(e)) ==> contains(e));

14 @ ensures (\forall Entry e; contains(e) ==>

16 (\old(contains(e)) || (e.getKey() == key &&

17 e.getValue() == value)));

18 @ ensures \result == \old(get(key));

19 @*/
20 public Object put(/*@ nullable @*/ Object key,
21 /*@ nullable @*/ Object value);

As the theMap model field is contained within the data group of the more general
objectState model field, the assignable clause is simply saying other fields from
the object could be modified as a result of changing the map. Although this is
reasonable for a general implementation, as JML allows heterogeneous frames,
we could not follow precisely why it is that theMap was not used directly, instead.
Again the use of an existential quantifier, and the has method of theMap ,instead
of the contains model method as a precondition (lines (3-5)) was surprising.
The postcondition specifies (line (13)) that all old entries be still in the map. In
lines (14-17), the specification states that known entries either did not change,
or were modified according to the new given key-value mapping parameters.
These two postconditions are consistent with the use of relational overriding
( ) in the Z model. Still, as the contains model method specification is empty,

these two postconditions on old entry containment are meaningless. The last
postcondition (line (18)) states that the result is the old value stored under
the given key. If there were no mappings for the key, or if the key is null ,
the result is null . Otherwise, the result is the previous value stored under the
given key. Furthermore, it seems that JML does not specify any concern with
respect to the two levels of injectivity that hm and Entry capture from the Java
documentation. As it involves handling null objects, this is the only place where
the Z model does not enforce one of the JML postconditions. Despite this fact,
we could easily add this with an additional predicate in the Put schema, such as

⊕

ContainsKey ⇒ GetValue

provided we added an additional val ! ∈ VID output variable to the Put decla-

ration list.

3.3 Operation Preconditions

The preconditions for operations are summarised in Table 1 below. Apart from
initialisation, the map operations rely on the HM invariant holding as part of
their precondition. That is, if the HashMap can be instantiated at all, then those
are the preconditions for the operations. The interesting and less obvious pre-
condition is for the hash map initialisation. It requires the existence of a map