previous up next
Go backward to A.2 The Invariant
Go up to A Proving Assertions
Go forward to A.4 Termination
RISC-Linz logo

A.3 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'.


Maintainer: Wolfgang Schreiner
Last Modification: November 14, 1997

previous up next