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

public class Display {
// Display represents the manager of the display.
// There is exactly one instance of Display per MIDlet
//@ public non_null ghost MIDlet midlet;
//@ public non_null ghost Displayable current;
//@ public non_null ghost Alert preAlert;
//@ ensures \result != null && \result.midlet == m;
//@ assignable \nothing;
public /*@pure@*/ static Display getDisplay(/*@non_null@*/ MIDlet m);
//@ ensures current == nextDisplayable && preAlert == null;
//@ assignable current, preAlert;
public void setCurrent(/*@non_null@*/ Displayable nextDisplayable);
//@ ensures current == nextDisplayable && preAlert == alert;
//@ assignable current, preAlert;
public void setCurrent(/*@non_null@*/ Alert alert,
/*@non_null@*/ Displayable nextDisplayable);
}
For the second setCurrent method we made a practical simplification. This
method causes an alert screen to be displayed temporarily (either with a
time-out or with a confirmation button) before updating the display to show
nextDisplayable . This could be specified by writing a complex specification
that keeps track of the sequence of displayed screens, including these alerts.
However, verification would be much more dicult and with little added value.
Instead, we introduce a ghost field, preAlert , which records that an alert screen
is temporarily displayed. So currents tracks the displayables being shown over
time, ignoring temporary Alert displayables.
To specify the GUI behaviour, we also have to specify the Displayable class
that represents particular screens on the display and the Command class that
represents input events. To simplify things we assume that each Command object
is bound to only one Displayable . Generally, this does not have to be the case
(commands can be reused through different displayables). However, in practice
most midlets define separate commands for each screen, and requiring it makes
verification simpler, as we do not need to use sets (or some representation of sets
such as lists) to track the set of displays associated with a command, and then
use set theory in verification. As for command listeners, the platform enables
only one per screen:
public class Command {
// The (only) Displayable object this command is attached to
//@ public ghost Displayable displayable;
}
public class Displayable {
//@ public ghost CommandListener commandListener;