Check out the new USENIX Web site. next up previous
Next: Observers Up: Specifications for Messages Previous: Effect of a Message

Effect of a Message on Observers

The behavior of a given message is further captured by specifying the return values of observers affected by the updates caused by it.

These are given using the interpretations clause with formulas of the form

interpretations g(y1, ..., yk) = h(xi1, ..., xil, y1, ..., yk)
if p(xi1, ..., xil, y1, ..., yk)

where h can be another observer of the same interface, an arithmetic, relational or logical operator or one of the operators on sequences of messages discussed below.

The meaning of the above formula is that, after an invocation m(c1, ..., cn), the return value of the message g(d1, ..., dk) will be equal to the value of the expression h(ci1, ..., cil, d1, ..., dk) evaluated after the message m(c1, ..., cn) terminates normally and p(ci1, ..., cil, d1, ..., dk) evaluates to true.

If the return value of an observer is not in the set of interpretations defined, it returns the same value as it before the invocation of m(c1, ..., cn).

A specification for a message is not well-formed if there is an enabled message whose interpretation is not defined.


next up previous
Next: Observers Up: Specifications for Messages Previous: Effect of a Message
Sreenivas Viswanadha
1998-03-17