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

Morgan's refinement calculus [25] ( i.e., L :[ P , Q ]). The list of locations L is the
frame; the precondition P is a predicate on the before-state; the postcondition Q
is a predicate on both the before and the after-states. Both conditions can refer
to attributes outside the frame, but the postcondition cannot change them. A
before-variable x in L appearing in Q is represented as \old(x) where an after-
variable is just x .Inthe signals clause, R represents the postcondition whenever
m() throws the exception E . This enables the specification of error cases much
like that in Z, where schema disjunction is used to combine error-free behaviour
with error handling (see the Disjoin Errors Z specification pattern in [37, p. 63]).
Default values are widely used in the case where some of JML clauses are
absent. In this way, no matter how minimal the given specification is, there is
always a version of it that JML tools can infer; this transformation of the various
syntaxes is known in the JML literature as “desugaring” [30]. We see the link
with Z as “sweetening” JML with (“calorie free”) results from proven theorems.

2.1 JML Type System

JML annotations include all expressions available in Java together with bounded
quantifiers. This includes reference to object attributes and some methods and
constructors, important since JML annotations were tailored for the Java pro-
grammer. Evaluating such expressions must not change the underlying object
state; otherwise they would compromise the Java code they are supposed to
specify. To help write side-effect free predicates, JML provides a meta-type sys-
tem with useful side-effect free data types defined as Java classes. This is based
on the JMLType class, which is the superclass of all meta-type systems. This
makes it possible to have sets, sequences, bags, and other mathematical objects
within JML annotations and quantifiers, just like one would expect to find in
other formal notations, such as Z's mathematical toolkit [34, Chap. 4].
One concern JML needs to address is how the various forms of object equality
in Java relate to the set-theoretic notion of equality. The two most important
notions of equality in Java are object identity equality ( i.e., o1 == o2 ), which is
like Leibniz's equality, and structural type equality ( i.e., o1.equals(o2) ), where
the former is usually stronger than the latter ( o1 == o2 ⇒ o1.equals(o2) ).
Other notions of equality are also important, such as serial (marshalled) equality
when object instances are represented as binary data files implementing the
Serializable interface, but we are not concerned with this for now. Structural
equality should be both symmetric and side-effect free, but this may not be the
case. A structural equality test may inadvertently cause side effects on the object
state; an alarming thought, since multiple consecutive calls to equals ought to
produce the same result.
The JML type system provides implementations that use both forms of equal-
ity. These facilities are essential in order to extend Java expressions with quan-
tifiers and set comprehension. Among these implementations, there are also
versions of sets that are “mathematical sets”, as opposed to a “collection of
objects”. That is, the JML type system offers for each meta-type, say a set,
four different implementations: collections of Object elements compared using