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

public class Display {
//@ public static ghost boolean displayUpdated;
//@ ensures current == nextDisplayable && preAlert == null;
//@ ensures Display.displayUpdated;
//@ assignable current, preAlert, Display.displayUpdated;
public void setCurrent(/*@non_null@*/ Displayable nextDisplayable); }
/*@ invariant Display.displayUpdated ==>
display.current == Options.opts.form ||
display.current == FinalScore.displayable || ...; @*/
By setting Display.displayUpdated to false we can temporarily 'switch off'
the invariant. The specification of setCurrent ensures that the guard is re-
established, so that the invariant has to hold after every call to setCurrent .
Screen Transitions. The invariant above suces to limit the set of screens
of a given midlet. In the next step we need to specify when and how screen
transitions happen. In general, this is a very dicult problem: midlets are con-
current applications and screens can be changed by the J2ME environment at
any time without user interaction. A notable example of this is an incoming
call on a mobile phone, or simply midlet environment warning screens, e.g. to
confirm sensitive operations. Note that we have already skipped such screens in
the specifications above, and in the navigation graph too. The non-deterministic
character of such screens would make the graph and the specification unneces-
sarily complex. Furthermore, we are interested in verifying the application itself
rather than the whole environment it runs in.
Apart from the cases mentioned above, the midlet screen transitions are trig-
gered by user input and actions. All user actions are handled by different im-
plementations of the commandAction method. This is where we add annotations
to limit the possible screen changes. The precondition limits the set of com-
mands that can be invoked on this screen, the postcondition describes how the
FinalScore screen will change after processing the command:
//@ requires c==cmd_yes || c==cmd_no;
//@ requires next == midlet.mainMenu.list;
//@ ensures c==cmd_no ==> midlet.display.current == next;
//@ ensures c==cmd_yes ==>
midlet.display.current == SendScores.displayable;
//@ assignable ...;
public void commandAction(Command c, Displayable d) {
if (c == cmd_no) {
midlet.getDisplay().setCurrent(next); }
else if (c == cmd_yes) {
SendScores sendScores = new SendScores(midlet);
sendScores.show(score, next); }
}