Go backward to Source Code Go 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: {
        msg = in(index).receive();
        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
      (out_j(0).length = 0, out_j(1).length = 0,
      ~sent_j, msg_j = null, state_j = 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 :<=> sent₀ => C(2)
C(c) :<=> c = Sum_j (out_j(0).length + out_j(1).length + n_j)
         where
             n_j = 0, if msg_j = null
             n_j = 1, else

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

S_j⁰ :<=> state_j = 0 =>
   msg_j = null, j=0 => (C(0), ~sent₀).
S_j¹ :<=> state_j = 1 =>
   msg_j = null, j = 0, C(0), ~sent₀.
S_j² :<=> state_j = 2 =>
   msg_j = null, j = 0, C(1), ~sent₀,
   out_j(1).length = 0.
S_j³ :<=> state_j = 3 =>
   msg_j = null.
S_j⁴ :<=> state_j = 4 =>
   msg_j = null.
S_j⁵ :<=> state_j = 5 =>
   msg_j = null, i_j < 5.
S_j⁶ :<=> state_j = 6 =>
   msg_j = null, i_j < 5,
   index_j in {0, 1}, in_j(index_j).length > 0.
S_j⁷ :<=> state_j = 7 =>
   msg_j /= null, i_j < 5,
   index_j in {0, 1}.
S_j⁸ :<=> state_j = 8 =>
   msg_j = null.

We will prove a generalized invariant I' defined as

I' :<=> I, forall j, k (S_j^k)

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 (S_j⁰) (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 S_j^k; 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 S_j^k is potentially affected by the transition.

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

• Assume state_j = 0: I is true after the transition, because sent₀ 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:
  • state_j = 1 => S_j¹: S_j¹ holds because the premise implies that the "then" path of the conditional was taken and thus j = 0 holds.
  • state_j = 3 => S_j³: S_j³ follows from S_j⁰ and the code.
• Assume state_j = 1: I is true after the transition, because sent₀ remains false. From S_j² we know j = 0 which implies that S_j'⁰, S_j'¹, S_j'² remain true for j' /=j. The only effect of the the send operation to some node j' /=j might be the invalidation of S_j'⁶. 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 in_j'(i).length > 0 cannot become false.

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

• Assume state_j = 2: we have to show that I remains true. By same reasoning as for the previous case, we get out_j(1).length = 1 after the transition. Together with C(1) and out_j(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 S_j'^k is affected by the transition. That S_j³ holds after the transition follows directly from the code and from S_j².

• Assume state_j = 3: from the code, the truth of I is self-evident, no S_j'^k is affected and by S_j³ also S_j⁴ is clear.
• Assume state_j = 4: it suffices to prove that the following conditions hold after the transition:
  • state_j = 5 => S_j⁵: i < 5 holds because the premise implies that the "then" part of the conditonal was taken.
  • state_j = 8 => S_j⁸: this is self-evident.
• Assume state_j = 5: the truth of I is clear and index_j is not referenced in any S_j'^k with j' /=j. Thus it suffices to show that S_j⁶ 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 S_j⁵, the truth of S_j⁶ is clear.
• Assume state_j = 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 S_j⁶ and knowing out.getSize() = 2 it is clear that, for some k in {0, 1} and non-negative l,

  in_j(k).length = 1+l

  holds before the transition, and that

  in_j(k).length = l, msg_j /= null

  holds after the transition and that k = index_j (both before and after the transition). From this and from the overall relationship between input and output channels

  Sum_j (in_j(0).length + in_j(1).length) =
  Sum_j (out_j(0).lenght + out_j(1).length)

  it is clear that I holds after the transition.

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

  From S_j⁶ and by above relationship between input and output channels we know before the transition out_j'(p).length > 0 for some j' /=j and p in {0, 1} (by network construction). Thus state₀ /=0, state_j' /=1 (for all j' /= j) and the transition cannot invalidate S_j'⁰ and S_j'¹. S_j'² 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. S_j'⁶ remains true because the truth of in_j'(index_j').length > 1 cannot be changed by a receive operation in j.

• Assume state_j = 7: the truth of I is clear from the fact that msg_j 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 S₀^j', S_j'¹ and S_j'² remain true. S_j'⁶ remains true because the truth of in_j'(index_j').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.