Information Technology Reference
In-Depth Information
About
launch
Stop logo animation
Defaults
OK
About
OK, Cancel
Main
Options
Exit
Options
OK
New
Alert (error)
Cancel
[SMS*]
Continue
Back
Alert (sent)
Wait (load)
Wait (sms)
[SMS]
No
error
[SMS]
Question
Wait (Sending)
[HTTP]
Select Answer
Error
error
[HTTP*]
error
OK
error
Final Score
Wait (load PIM)
Send Scores
Yes
[PIM]
Fig. 6.
State diagram: navigation graph for the Mobius game
the
CommandListener
interface to handle user actions. The class
QuizQuestion
encapsulates a single quiz question and a displayable object for this question.
Finally, there are two utility classes that handle network connections and PIM
access. The whole application consists of 13 small classes.
We start with specifying possible screens and screen transitions of our midlet.
As it turns out this is the more dicult part and also one that exhibits the
biggest problems with accurate specification of the navigation graph in JML.
Later we deal with the calls to sensitive operations.
Screen State.
To specify the navigation graph accurately we need to keep track
of screen changes in our midlet. For this we use the
current
instance field of
the
Display
object associated with our midlet. A suitable invariant enforces the
limit on the set of possible screens, as follows:
public class QuizMidlet extends MIDlet {
private /*@ spec_public non_null @*/ Display display;
private /*@ spec_public non_null @*/ MainMenu mainMenu;
/*@ invariant display.current == mainMenu.list ||
display.current == About.about.alert ||
display.current == Options.opts.form ...;
@*/
However, we quickly run into problems with completing this invariant, because
for every screen - i.e.
Displayable
- the application uses we need some program
variable (like
mainMenu.list
) to refer to it. Such variables do not always exist.
Some objects of type
Displayable
are created on the fly, and cannot be referred
to from the class
QuizMidlet
. For example, this is the case for the
FinalScore
screen in the game, which is created locally in the
MainMenu
class:
Search WWH ::
Custom Search