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

MessageConnection

Connector Connection

open() : Connection

HttpConnection

Fig. 3. Class diagram: network connection related API

PIM PIMList PIMItem

1 0..*

getInstance() : PIM
openPIMList() : PIMList

items() : Enumeration<PIMItem>

ContactList Contact

Fig. 4. Class diagram: personal information related API

establishing different kinds of network connections (SMS, Internet), and a few
classes that encapsulate these different connections, like MessageConnection or
HttpConnection . Fig. 3 gives a simplified view.
For personal information management (PIM) there is one utility class PIM
that provides methods for accessing the phone book (contact list), and a few
classes that represent a single contact or the whole contact list (Fig. 4).

3 Navigation Graphs

In [5] two formalisations are given to deal with midlet navigation graphs. The first
formalisation deals with the MIDP GUI structure. We described it intuitively
using UML. In [5] a more detailed semantics is given in terms of the Bicolano
semantics[18]ofJavabytecode;therethe formalisation of the GUI is needed to
develop the algorithm to generate navigation graphs out of bytecode. For our
purposes the lightweight UML representation of the GUI is sucient to represent
the GUI behaviour in JML by annotating the parts of the MIDP API dealing
with the GUI. Although we do not use the detailed formalisation of the GUI
from [5], there is a close correspondence between that formalisation and our JML
representation of the graphs. E.g., our 1

0 .. 1 relation between Displayables
and CommandListeners is the relation g. list in [5], where g denotes the state
of the GUI and the whole relation maps CommandListeners to Displayables .
Similarly, the relation g. coms in [5] corresponds to our 1

−

− 0 ..∗ mapping between

Displayables and Commands .
The second part of the formalisation in [5] gives a formal definition of a midlet
navigation graph itself. Putting aside the complex notation, a midlet navigation
graph is essentially an oriented multigraph. The nodes of this graph are possi-
ble midlet states, i.e. different application screens. The arrows of the graph are