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

Sensitive Operations. In the last step we limit the sensitive operations our
midlet performs. For any method that ultimately calls down to one of these
operations we need to add a contract for the associated ghost variable that, as
described at the end of Sect. 4.1, tracks the number of invocations.
//@ ensures Connector.openCount == \old(Connector.openCount);
public void commandAction(Command c, Displayable d) { ... }
Then we allow the sensitive operations to be performed by the implementations
of the commandAction that correspond to transitions in the graph:
public class SendScores {
//@ ensures c == cmd_ok ==>
MessageConnection.smsSent <= \old(MessageConnection.smsSent) + 1;
//@ assignable MessageConnection.smsSent, ...;
public void commandAction(Command c, Displayable d) {
... else if (c == cmd_ok) {
WaitAlert.getInstance().show(midlet, Consts.SENDING_RESULT);
String s = numberField.getString();
sendSMS(s); ... }
}
}
A similar approach is used to limit access to personal data (e.g. the phone book)
in the MIDP environment.
If properties are expressed in postconditions, we have to consider the issue
of non-termination. Verification would have to be done using total correctness
to ensure that, say, limits on the number of SMS sent are not broken in non-
terminating executions of a method. Still, for commandAction methods which
do not have the MessageConnection.smsSent in their assignable clause, the
contract does rule out that any SMS are sent in non-terminating executions.
5 Specification and Verification Issues
During the verification of this case study with ESC/Java2 two practical issues
surfaced. The first one has to do with singleton pattern classes, the second one
with visible state semantics of invariants.
Singleton Objects. Many classes in midlet code study and in the MIDP API
follow the singleton pattern [8], i.e. only one instance of these classes is ever cre-
ated. Knowing that a class is only ever going to have a single instance could in
principle simplify reasoning. However, specifying that a class follows the single-
ton pattern in JML, and verifying it with ESC/Java2, can be a bit clumsy. E.g.,
specifying that Options is a singleton class could be specified by an invariant
private /*@ spec_public @*/ static Options instance = null;
//@ invariant this == instance;