Go backward to Source CodeGo up to Top

# Correctness Proof

We are going to formally verify the assertion stated by the program: as soon as node 0 has signalled by its variable `sent` the initialization of the network, there must be exactly two messages in the network.

#### State Transitions

For the purpose of verification, we rewrite the method `main` as follows:

```public void main()
{
int i;
int state = 0;
while (state != 8) {
switch (state) {
case 0: {
if (number = 0)
state = 1;
else
state = 3;
}
case 1: {
out(0).send(new Msg(0));
state = 2;
}
case 2: {
out(1).send(new Msg(0))
sent = true;
state = 3;
}
case 3: {
i = 0;
state = 4;
}
case 4: {
if (i < 5)
state = 5;
else
state = 8;
}
case 5: {
index = in().select();
state = 6;
}
case 6: {
state = 7;
}
case 7: {
out(index).send(msg);
msg = null;
i = i+1;
state = 4;
}
}
}
}
```

This program implements the same behavior as the original one presented in the previous subsection by a sequence of state transitions such that the only interaction with other nodes (`send`, `receive`, `select`) occurs as the first statement of some transition. A node program may be interrupted only immediately before such a communication operation takes place. Network execution can be therefore considered as an interleaving of such transitions from the programs of different nodes.

#### The Invariant

To establish the truth of a global invariant, it thus suffices to prove

A => I
I =>o I

where A describes the initial state of the network (immediately before the transition loop is entered) and the implication I =>o I denotes the invariance of I on every state transition (i.e., if I holds immediately before the transition, it must also hold after the transition).

The initial condition A of our network is defined as

A :<=>
forall j
(outj(0).length = 0, outj(1).length = 0,
~sentj, msgj = null, statej = 0)

i.e., all channels are empty, the local variables are initialized as described by the program constructor, and programs start with initial state 0.

We want to prove invariant I defined as

I :<=> sent0 => C(2)
C(c) :<=> c = Sumj (outj(0).length + outj(1).length + nj)
where
nj = 0, if msgj = null
nj = 1, else
which is exactly the assertion implemented in the previous section. A subscripted variable vj denotes the content of variable `v` in program `j` (j is represented in the program by the variable `number`). outj(i) denotes the array of messages `out(i).getMessages()` in program j.

For the purpose of verification, we need a couple of auxiliary propositions that describe the state at the beginning of each transition:

Sj0 :<=> statej = 0 =>
msgj = null, j=0 => (C(0), ~sent0).
Sj1 :<=> statej = 1 =>
msgj = null, j = 0, C(0), ~sent0.
Sj2 :<=> statej = 2 =>
msgj = null, j = 0, C(1), ~sent0,
outj(1).length = 0.
Sj3 :<=> statej = 3 =>
msgj = null.
Sj4 :<=> statej = 4 =>
msgj = null.
Sj5 :<=> statej = 5 =>
msgj = null, ij < 5.
Sj6 :<=> statej = 6 =>
msgj = null, ij < 5,
indexj in {0, 1}, inj(indexj).length > 0.
Sj7 :<=> statej = 7 =>
msgj /= null, ij < 5,
indexj in {0, 1}.
Sj8 :<=> statej = 8 =>
msgj = null.

We will prove a generalized invariant I' defined as

I' :<=> I, forall j, k (Sjk)
from which I trivially follows.

#### The Proof

We are now going to prove

A => I'
I' =>o I'

For proving A => I', it suffices to prove A => I and A => forall j (Sj0) (both of which are direct consequences of A).

For proving I' =>o I', we have to establish the truth of I after the transition and to show Sjk; it suffices to consider only those j, k where

1. j is the index of the current node and k denotes a potential successor state of the transition, or
2. j is the index of another node and Sjk is potentially affected by the transition.
In our program, the second case is only relevant for Sj0, Sj1, Sj2 (because they contain propositions about all nodes) and Sj6 (because it contains a proposition about the state of the node interface inj which may be changed by some `send` operation).

We proceed by case distinction on the current state of node j, i.e., on the value of statej:

• Assume statej = 0: I is true after the transition, because sent0 remains false. Since the transition does not involve a `send` or an assigment operation, nodes other than j are not affected. There are two potential successor states; it thus suffices to prove that the following conditions hold after the transition:
• statej = 1 => Sj1: Sj1 holds because the premise implies that the "then" path of the conditional was taken and thus j = 0 holds.
• statej = 3 => Sj3: Sj3 follows from Sj0 and the code.
• Assume statej = 1: I is true after the transition, because sent0 remains false. From Sj2 we know j = 0 which implies that Sj'0, Sj'1, Sj'2 remain true for j' /=j. The only effect of the the `send` operation to some node j' /=j might be the invalidation of Sj'6. However, the statement
```c.send(m)
```
satisfies the transition rule
c = q =>o c = q:m
(i.e., it appends one element m to the message queue q of channel c), thus inj'(i).length > 0 cannot become false.

It remains to be shown that statej = 2 => Sj2 after the transition. From C(0) at the beginning of the transition, we know outj(1).length = 0, which remains true. Furthermore, by above transition rule, we can easily deduce outj(0).length = 1 and thus C(1) after the transition.

• Assume statej = 2: we have to show that I remains true. By same reasoning as for the previous case, we get outj(1).length = 1 after the transition. Together with C(1) and outj(1).length = 1 at the beginning of the transition, we can deduce C(2) after the transition.

By same reasoning as for the previous case, no Sj'k is affected by the transition. That Sj3 holds after the transition follows directly from the code and from Sj2.

• Assume statej = 3: from the code, the truth of I is self-evident, no Sj'k is affected and by Sj3 also Sj4 is clear.
• Assume statej = 4: it suffices to prove that the following conditions hold after the transition:
• statej = 5 => Sj5: i < 5 holds because the premise implies that the "then" part of the conditonal was taken.
• statej = 8 => Sj8: this is self-evident.
• Assume statej = 5: the truth of I is clear and indexj is not referenced in any Sj'k with j' /=j. Thus it suffices to show that Sj6 holds after the transition. The statement
```i = s.select()
```
satisfies the transition rule
s.getSize() > 0 =>o 0 <= i < s.getSize(), s(i).length > 0
and we know by network construction out.getSize() = 2. Thus, using Sj5, the truth of Sj6 is clear.
• Assume statej = 6: first we show the truth of I after the transition. The statement
```m = c.receive()
```
satisfies the transition rule
c = n:q =>o m = n, c = q
(for some non-null message n and message queue q). From this and Sj6 and knowing out.getSize() = 2 it is clear that, for some k in {0, 1} and non-negative l,
inj(k).length = 1+l
holds before the transition, and that
inj(k).length = l, msgj /= null
holds after the transition and that k = indexj (both before and after the transition). From this and from the overall relationship between input and output channels
Sumj (inj(0).length + inj(1).length) =
Sumj (outj(0).lenght + outj(1).length)
it is clear that I holds after the transition.

By above reasoning, it is also clear that Sj7 holds after the transition.

From Sj6 and by above relationship between input and output channels we know before the transition outj'(p).length > 0 for some j' /=j and p in {0, 1} (by network construction). Thus state0 /=0, statej' /=1 (for all j' /= j) and the transition cannot invalidate Sj'0 and Sj'1. Sj'2 remains true because `out`j'(1).length() = 0 cannot be changed by a `receive` operation; furthermore I and C(1) at the beginning of the transition implies by the code and above rule also C(1) at the end of the transition. Sj'6 remains true because the truth of inj'(indexj').length > 1 cannot be changed by a `receive` operation in j.

• Assume statej = 7: the truth of I is clear from the fact that msgj is non-null before the transition but null after the transition using the transition rule for `send` shown above.

Similar reasoning as in the previous case also shows that S0j', Sj'1 and Sj'2 remain true. Sj'6 remains true because the truth of inj'(indexj').length > 1 cannot be changed by a `send` operation.

Thus we have established the invariance of I'.

#### Termination

Since each program loops through a bounded number of iterations, it is clear that the execution of the network will not run forever. It is however less clear whether all node programs actually reach the termination state. In fact, this is not guarantueed: two network programs may terminate in a state where both messages are captured in the channels between them; the third node will thus wait forever on its input channels.

Maintained by: Wolfgang Schreiner
Last Modification: November 14, 1997