previous up next
Go backward to Source Code
Go up to Top
RISC-Linz logo

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;
          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;
          state = 8;
      case 5: {
        index = in().select();
        state = 6;
      case 6: {
        msg = in(index).receive();
        state = 7;
      case 7: {
        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)
             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:

Thus we have established the invariance of I'.


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

previous up next