Midlet Navigation Graphs in JML - Formal Methods: Foundations and Applications - page 28

saying that all Options objects are equal to the static instance . However, this
invariant is typically too strong, given the visible state semantics of invariants.
If the singleton object is created by a static get-method as is done in the code,
e.g.
//@ ensures \result != null && \result == instance;
//@ assignable Options.instance;
public static Options getInstance() {
if (instance == null) instance = new Options();
return instance;
}
then the constructor call new Options() by itself does not establish the invari-
ant, as it will not hold till after the assignment to instance .
A possible solution is to make the constructor a helper:
public /*@ helper @*/ Options() {...}
effectively telling ESC/Java2 to inline calls to the constructor, but it turns out
that ESC/Java2 reasons in a rather unpredictable way when a private construc-
tor is declared as helper .
In the end we let ESC/Java2 complain about the possibly unsatisfied this
== instance invariant after a call to new Options() in getInstance() and
suppressed this warning with the @nowarn directive.
It would be nice to have a standard, e.g. following ideas from [19], simple way
of specifying singleton behaviour in JML, so that no necessary complications
and side conditions are introduced during reasoning.
Visible State Semantics of Invariants. JML uses the visible state semantics
for object invariants [13]. This means that all invariants of all objects of all types
have to hold in all visible states , which includes all post-states of constructor calls
and all pre- and post-states of method calls 5 .
This semantics makes verification very hard, and non-modular 6 :whenverify-
ing a method in one class one should take into consideration breaking invariants
of other objects, of any class, that happen to be allocated. To enable modular
verification, ESC/Java [7] uses a slightly weaker and potentially unsound seman-
tics. ESC/Java2 [11] uses the same semantics, but now includes features to warn
users about potential problems [12,10].
Working on the case study, this generated several false positives, where the
code was incorrectly deemed to be correct. The root of the problem was that
when checking code that calls API methods, ESC/Java2 will assume that these
API methods preserve all invariants. When checking the implementation of these
API methods the tool would probably warn that they do not preserve invariants,
5 Except those constructors and methods designated as helper 's.
6 However, the semantics is sound, unlike more simple-minded semantics for object
invariants!