Comments on "On the proof of a distributed algorithm" : always-true is not invariant

We would like to report an error in a proof given by J.-P. Verjus in [3]. More importantly, we would like to point out a difference between the notions "always-true" and "invariant", which are identified in [3]. In his paper, Verjus claims that invariance proofs by contradiction are shorter than invariance proofs by the established method, called the "induction method" in [3]. To illustrate his idea, he proposes an alternative correctness proof for a termination detection algorithm given by Dijkstra, Feijen, and Van Gasteren [2]. We show that his—operational—proof is incorrect and incomplete (Section 1); moreover, what he shows is that a predicate is always-true, which is strictly weaker than invariance (Section 2). Instead of illustrating the merits of proofs by contradiction, the proof strongly supports our opinion that operational arguments should be avoided.