previous up next
Go backward to A.1 State Transitions
Go up to A Proving Assertions
Go forward to A.3 The Proof
RISC-Linz logo

A.2 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.
Maintainer: Wolfgang Schreiner
Last Modification: November 14, 1997

previous up next