A.1 Protocol Variables
The protocol is expressed in terms of the following program variables:
- S: String
- denotes the current status of the program.
- T: String
- denotes a substatus, i.e., a refinement of the
current status; T may take the special constant `null'.
- version: String
- identifies the version of the protocol that
the application program understands.
- taskStack: Array[Message]
- denotes the stack of task
messages that were received by the external application program and for which
it has not yet delivered corresponding results; a result may be only delivered
for the task on the top of the stack.
- taskDepth: Natural
- denotes the number of elements on the
task stack.
- waitStack: Array[Message]
- denotes the stack of wait
messages that were sent by the external application program and for which it
has not yet received corresponding replies; a reply can be only received for
the wait message on the top of the stack.
- waitDepth: Natural
- denotes the number of elements on the
wait stack.
- taskId: TaskId
- describes the identifier used to denote the
next task to be created.
- taskMin: TaskId
- describes the lower bound of the range of
identifiers that may be used to denote new tasks.
- taskMax: TaskId
- describes the upper bound of the task
identifier range.
We use the following types in variable annotations of the form v:
T to assert that v must be an element of the set T:
- String
- An arbitrary sequence of characters not including the
newline character.
- Command
- A string that may be evaluated as a command by the
application program.
- Expression
- A string that may be evaluated as an expression by the
application program.
- Integer
- An integer number.
- Natural
- A non-negative integer number.
- TaskId
- A natural number that identifies a task.
- Array[T]
- An indexable array of elements of type T.
- Message
- A record m such that m.key is a
string denoting the type of a message and m.body is an array of
strings.
In our protocol specification, Integers are implicitly converted to strings
(using thee textual representation of an integer as its string
encoding). Likewise we assume that there is some encoding of commands and
expressions as strings.
Maintainer: Wolfgang Schreiner
Last Modification: July 6, 2001