The design of Igloo is shown in figure 4.1. The architecture is intended to be one of the client/server style, though as we shall see later this is currently incomplete. Major modules in the system are:
![\includegraphics[width=6in]{igloo.eps}](img11.png)
Igloo is a based upon the client/server model of computation.
The actual computation is handled by
Isabelle.
Since
Isabelle does not provide any means for
network connections we have designed a small server that listens
for remote connections, and upon success, executes
a copy of Isabelle and begins shovelling data to and from the
client.
|
The Communicator module handles the transport of data to and from Isabelle. This may be either network or local communication. More detail is given in §4.4
The Isabelle Server (§4.7) listens for connections, and runs an instance of Isabelle once the user connects. It also provides a method of secure authentication, and may be trivially extended to provide encryption.
The Mediator module (§4.5) coordinates the events that occur as messages are received from Isabelle, and also turns requests from the GUI into messages of the correct format to be sent to Isabelle.
Other notable classes are those involved in the manipulation of PGIP and PGML messages which are used to describe proof states and operations that map from one proof state to another, are described in section 4.6.
|
|
|