Go backward to A.2 The Invariant Go up to A Proving Assertions Go forward to A.4 Termination

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 (S_j⁰) (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 S_j^k; 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 S_j^k is potentially affected by the transition.

We proceed by case distinction on the current state of node j, i.e., on the value of state_j:

• Assume state_j = 0: I is true after the transition, because sent₀ remains false. Since the transition does not involve a send or an assigment operation, nodes other than j are not affected. There are two potential successor states; it thus suffices to prove that the following conditions hold after the transition:
  • state_j = 1 => S_j¹: S_j¹ holds because the premise implies that the "then" path of the conditional was taken and thus j = 0 holds.
  • state_j = 3 => S_j³: S_j³ follows from S_j⁰ and the code.
• Assume state_j = 1: I is true after the transition, because sent₀ remains false. From S_j² we know j = 0 which implies that S_j'⁰, S_j'¹, S_j'² remain true for j' /=j. The only effect of the the send operation to some node j' /=j might be the invalidation of S_j'⁶. However, the statement

  c.send(m)
  

  satisfies the transition rule

  c = q =>_o c = q:m

  (i.e., it appends one element m to the message queue q of channel c), thus in_j'(i).length > 0 cannot become false.

  It remains to be shown that state_j = 2 => S_j² after the transition. From C(0) at the beginning of the transition, we know out_j(1).length = 0, which remains true. Furthermore, by above transition rule, we can easily deduce out_j(0).length = 1 and thus C(1) after the transition.

• Assume state_j = 2: we have to show that I remains true. By same reasoning as for the previous case, we get out_j(1).length = 1 after the transition. Together with C(1) and out_j(1).length = 1 at the beginning of the transition, we can deduce C(2) after the transition.

  By same reasoning as for the previous case, no S_j'^k is affected by the transition. That S_j³ holds after the transition follows directly from the code and from S_j².

• Assume state_j = 3: from the code, the truth of I is self-evident, no S_j'^k is affected and by S_j³ also S_j⁴ is clear.
• Assume state_j = 4: it suffices to prove that the following conditions hold after the transition:
  • state_j = 5 => S_j⁵: i < 5 holds because the premise implies that the "then" part of the conditonal was taken.
  • state_j = 8 => S_j⁸: this is self-evident.
• Assume state_j = 5: the truth of I is clear and index_j is not referenced in any S_j'^k with j' /=j. Thus it suffices to show that S_j⁶ holds after the transition. The statement

  i = s.select()
  

  satisfies the transition rule

  s.getSize() > 0 =>_o 0 <= i < s.getSize(), s(i).length > 0

  and we know by network construction out.getSize() = 2. Thus, using S_j⁵, the truth of S_j⁶ is clear.
• Assume state_j = 6: first we show the truth of I after the transition. The statement

  m = c.receive()
  

  satisfies the transition rule

  c = n:q =>_o m = n, c = q

  (for some non-null message n and message queue q). From this and S_j⁶ and knowing out.getSize() = 2 it is clear that, for some k in {0, 1} and non-negative l,

  in_j(k).length = 1+l

  holds before the transition, and that

  in_j(k).length = l, msg_j /= null

  holds after the transition and that k = index_j (both before and after the transition). From this and from the overall relationship between input and output channels

  Sum_j (in_j(0).length + in_j(1).length) =
  Sum_j (out_j(0).lenght + out_j(1).length)

  it is clear that I holds after the transition.

  By above reasoning, it is also clear that S_j⁷ holds after the transition.

  From S_j⁶ and by above relationship between input and output channels we know before the transition out_j'(p).length > 0 for some j' /=j and p in {0, 1} (by network construction). Thus state₀ /=0, state_j' /=1 (for all j' /= j) and the transition cannot invalidate S_j'⁰ and S_j'¹. S_j'² remains true because out_j'(1).length() = 0 cannot be changed by a receive operation; furthermore I and C(1) at the beginning of the transition implies by the code and above rule also C(1) at the end of the transition. S_j'⁶ remains true because the truth of in_j'(index_j').length > 1 cannot be changed by a receive operation in j.

• Assume state_j = 7: the truth of I is clear from the fact that msg_j is non-null before the transition but null after the transition using the transition rule for send shown above.

  Similar reasoning as in the previous case also shows that S₀^j', S_j'¹ and S_j'² remain true. S_j'⁶ remains true because the truth of in_j'(index_j').length > 1 cannot be changed by a send operation.

Thus we have established the invariance of I'.