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

but as we are only ever checking the midlet code - i.e. client code of the API -
and never implementation of this API, this issue can easily go undetected.
The example below illustrates this:
public class APIClass {
//@ requires array.length == 1;
//@ ensures array[0] == v; assignable array[0];
public static void setArray(/*@ non_null @*/ int[] array, int v);
}
public class ClientClass {
private /*@ non_null @*/ int[] values = {1};
//@ invariant values[0] == 1 && values.length == 1;
public void modifyArray() { APIClass.setArray(values, 2); }
}
Checking the modifyArray method with ESC/Java2 does not show any prob-
lems. However, it is clear that a call to APIClass.setArray breaks the class
invariant for ClientClass . However, the tool assumes that the API class will
re-establish all invariants.
Running the tool on an implementation of the setArray method would prob-
ably reveal that the invariant of ClientClass might be broken, but typically
one treats the API as a black box and one does not look at implementations of
it. Unfortunately the inconsistency warning of ESC/Java2 [12,10] does not catch
these situations.
Sound and modular verification techniques that cope with class invariants do
exist [6], and are for instance used in Spec# [1]. Some verification tools, like
KeY [3], allow a very flexible invariant semantics; there it is up to the user to
choose which class (or even method) is responsible for a given invariant, but that
means soundness is up to the user too.
6 Evaluation and Discussion
An issue often overlooked in research on program verification is coming up with
interesting properties to verify. We have shown a way to specify midlet navigation
graphs by means of JML annotations. This required some generic annotation of
the MIDP API, which provides a 'ghost state' to talk about the relevant platform
infrastructure - ghost fields that track which Displayable is being shown, and
hence which CommandListener is active, etc. - and contracts for some API calls
that describe their effect on this ghost state. An individual midlet can then be
annotated to express conformance to a midlet navigation graph, by introducing
an invariant that restricts the possible Displayable s that can be shown, and
contracts for commandAction methods that specify the screen transitions that are
allowed. Additional restrictions on security-sensitive API calls, saying in which
states these may occurs, can be expressed if API specifications for these methods
are added to track their usage.