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

public void quizFinished() {
int score = currentGame.getScore(); ...
FinalScore finalScore = new FinalScore(midlet, score);
finalScore.show(getDisplayable());
}
The finalScore object, the screen that displays the score, is only visible locally
in the quizFinished method and it cannot be referred to in a global midlet
invariant. There are other examples of such locally created displayables in the
midlet code.
To solve this problem we turn to static ghost variables. Although the prob-
lematic displayable objects are created locally, there is only one object of a given
kind created and possibly active at a time. So we simply store such locally cre-
ated displayable object in a static ghost variable. Since we can make the static
variable public it will be in scope for all our specifications. The fact that it is
static lets us make sure that we keep track of only the most recently (and thus
current) created displayable object of a given type, and also that access to this
ghost variable is object reference independent. For the FinalScore class the
relevant annotations are the following:
public class FinalScore implements CommandListener {
//@ public static ghost Alert displayable;
public void show(Displayable next) { ...
Alert alert = new Alert("Final Scores");
//@ set FinalScore.displayable = alert;
alert.setTimeout(Alert.FOREVER); ...
midlet.getDisplay().setCurrent(alert);
}
Then our invariant can refer to the FinalScore.displayable field:
/*@ invariant ... display.current == Options.opts.form ||
display.current == FinalScore.displayable || ... ; @*/
However, this solution brings up another problem. The visible state semantics
of invariants requires all invariants of all objects to hold in all visible states
(i.e. all pre- and post-states of all method calls) during the execution of our
midlet. This obviously does not hold in the code above. Our invariant is broken
in all the states between the state where FinalScore.displayable is set and
the state when the display is updated by invoking setCurrent .Intheseinter-
mediate states display.current may point to a reference that is not stored in
FinalScore.displayable anymore.
A (standard) trick we use to solve this problem is introducing a global boolean
guard, Display.displayUpdated , to switch invariants on and off at appropriate
points, as shown below.