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

The JML specification is similar.

1 /*+@ public normal_behavior
2 @ ensures \result <==> theMap.isEmpty();
3 @ implies_that
4 @+*/
5 /*@ public normal_behavior
6 @ ensures \result <==> (size() == 0);

7 @*/
8 /*@ pure @*/ boolean isEmpty();

Unfortunately, the implies that keyword is not documented in [24] or [30].
Another query operation retrieves the mapped value associated with a given
key ?, provided the key is contained in the map. The actual value ( val !) is the
result of applying the key ?tothe Entry injective sequence returned by the map
at the given index. As the pairs within ran s are functional, where s

Entry ,
we can apply it to key ? to retrieve the associated value. This creates interesting
(and possibly general) proof obligations about the result of ran, which is defined
as a relation, to be functional, so that application to key ? is well-defined.

∈

GetValue
KeyQueryOp ; val !: VID

ContainsKey
val !=(ran( hm idx )) key ?

Its JML specification is similar to the containment operations, but with the extra
requirement for key containment.

1 /*+@
2 @ public normal_behavior

3 @ requires containsKey(key);

4 @ ensures (\exists Entry e; theMap.has(e); e != null

5 @ && JMLNullSafe.equals(e.abstractKey, key)

6 @ && \result.equals(e.abstractValue));

7 @*/
8 /*@ pure @*/ Object get(/*@ nullable @*/ Object key);

The obvious difference is that now there is an extra equality condition (line (6))
about the method result ( val !) being the mapped value. As we are not consid-
ering null keys, we omit that part of the specification. Like in the key-value
containment operations, it is not quite clear why the ensures clause needs the
existential quantifier for a non-boolean method. We believe that is because there
was no specification for the model method contains mentioned above. We would
still need to investigate further with the JML community to clarify this precisely.
Similarly as before, we define general schemas now for insertion operations
with the MapOp schema.