Go up to A Proving Assertions Go forward to A.2 The Invariant

A.1 State Transitions

For the purpose of this subsection, 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.