Go backward to B.4 State ProgramGo up to B Distributed Snapshots |

We will prove the correctness of the program shown above; this is *not* a
proof of the Chandy-Lamport algorithm that solves a much more general
problem [6]. However, by focusing on our application, the proof
becomes more concrete and its relationship to the program more direct.

In this section, we wil use the following typed variables:

ma message ca channel, identified with the array of messages in it i,j indices of network nodes k an index of a message in c, 0 <=k <c.lengthh an index of a channel in a set s, 0 <=k <s.getSize()

Furthermore, we will denote by `d`_{i} >= 0 the initial value of
`deposit`_{i} and by `n` the number of nodes in the network.

Maintainer: Wolfgang Schreiner

Last Modification: October 1, 1998