Verification of a distributed summation algorithm

A correctness proof of a variant of Segall's Propagation of Information with Feedback protocol is presented. The proof, which is carried out within the I/O automata model of Lynch and Tuttle, is standard except for the use of a prophecy variable. The aim of this paper is to show that, unlike what has been suggested in the literature, assertional methods based on invariant reasoning support an intuitive way to think about and understand this algorithm.