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

//@ ensures cmd.displayable == this; assignable cmd.displayable;
public void addCommand(/*@non_null@*/ Command cmd);
//@ ensures commandListener == l; assignable commandListener;
public void setCommandListener(/*@non_null@*/ CommandListener l);
}
Finally, the specification of CommandListener should reflect the MIDP platform
guarantees, namely that the current displayable and command are not null, and
that the invoked command is in fact associated with the given displayable 4 :
public interface CommandListener {
//@ requires c.displayable == d;
//@ assignable \everything;
public void commandAction(/*@non_null@*/ Command c,
/*@non_null@*/ Displayable d);
}
If we trust the platform not to behave abnormally, these assumptions are safe.
For security-sensitive API calls, that may result in say network usage or ac-
cess to private information, we want our API specification to track the number
of invocations. For this we declare suitable static ghost variables to count the
number of invocations. This allows us to express restrictions on these numbers
in a specification for midlet. For example, for the open method of the Connector
class, which establishes new network or SMS connections, we can specify
public class Connector {
//@ public static ghost int openCount;
//@ ensures Connector.openCount == \old(Connector.openCount) + 1;
//@ assignable Connector.openCount;
public static Connection open(/*@non_null@*/ String name);
}
4.2 Midlet Annotations - The Mobius Case Study
We will present the JML annotations for midlets using the Mobius demonstration
midlet. The midlet implements a simple mobile phone quiz game. The security
sensitive operations of the quiz game are using an HTTP connection to download
game questions, sending answers and scores in SMS messages, and also accessing
the Personal Information Manager (PIM), i.e. the phone book. Fig. 6 shows the
complete navigation graph of this midlet.
The application class structure is as follows. There is a singleton class Quiz-
Midlet which is the main application container. Then there are several classes to
represent different screens of the game: main menu, options screen, about screen,
the main game screen, etc. Most of these classes use the Singleton pattern, mean-
ing there will only ever be a single instance of them. These classes also implement
4 The assignable \ everything clause in the spec means that classes implementing
this method are in principle free to have any side-effects.