Go backward to B.4 State Program Go up to B Distributed Snapshots

B.5 Verification

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:

m	a message
c	a 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.length
h	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.