Go backward to A.1 State Transitions
Go up to A Proving Assertions
Go forward to A.3 The Proof
|
Go backward to A.1 State Transitions Go up to A Proving Assertions Go forward to A.3 The Proof |
|
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)which is exactly the assertion implemented in the previous section. A subscripted variable vj denotes the content of variable
C(c) :<=> c = Sumj (outj(0).length + outj(1).length + nj)
where
nj = 0, if msgj = null
nj = 1, else
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.