Logic-based specifications

The general principles are well explained in Chapter 4 of Peled's book. (See Selected Reading Material for the course ELG-7187C; the key parts are here: modeling general transition systems (A, B, C) and an example (D, E))

Example 1: Queue of maximum length N

Here we only model the temporal ordering of the actions put and get, as we did with the LTS formalism.
Variable: int size;
Initially: size = 0
Transitions:
    put: size < N --> size := size + 1
    get: size > 0  --> size := size - 1

Example 2: Queue of maximum length N (including the values stored in the queue)

Variables :  int size;   ListOfElements content
Initially: size = 0 and content = emptyList
Transitions:
    put(Element e): size < N --> (size, content) := (size + 1,  content cat e)
    get(Element e): size > 0 and e = first(content) --> (size, content) := (size - 1,  tail(content))

Example 3: Queue with users

We consider the above queue and two users producer and consumer that execute the transitions put and get, respectively (that is, their transition of interest is directly coupled with the respective transition of the queue).
If we consider the Producer, the Consumer and the Queue communicating as defined above, we may prove the following invariant assertion: (Note: an invariant assertion is a predicate, depending on the state variable, that is always true in between the transitions of the system).

Note that the variables sendSequence and receiveSequence would probably not be included in an implementation of the producer and consumer components. They are introduced at this abstract level of description in order to define the semantics of the operations put and get. They are called history variables.

The proof of such an invariant can be done by induction over the number of transitions that have been executed within the overall system. (Note: this proof is very easy in this case; it is left as an exercise)

Other notation

In many cases another notation is used to define the enabling predicate and the conditions on the new values of the variables. One simply write a single boolean predicate which is the conjunction of the enabling predicate (which may be called the pre-condition) and the condition that the variables must satisfy after the execution of the transition (one may call this the post-condition). In the post-condition, however, one may have to refer to the variable values before and after the execution of the transition; in order to distinguish these two values, the new value is denoted by the name of the variable followed by " ' " , for instance, the transition put of Example 1 may be characterized by the condition: size < N and size' = size + 1 . This notation is used, for instance, by Z and TLA.

Composition

In Example 3, the composition of the three components (producer, queue, consumer) did not pose any problem because the variables of these components were disjoint. But let us assume that we want to compose two queues of length N (let us call them the left and the right queue) into a larger system by introducing internal (hidden) communication between these two queues by requiring that the get transition of the right-most queue is directly coupled with the put transition of the left-most queue. If the put transition of the right queue and the get transition of the left queue remain externally visible, it is clear that the composition will behave as a queue of length 2N. However, if we want to write this composition down, we have to distinguish the names of the variables of these two queues. Since they have the same name originally, we may want to rename them (e.g. leftSize and rightSize) before we do the composition. The internal, hidden transition will be assumed to be (spontaneously) executed whenever it is possible.

Last updated: January 17, 2008