TY - JOUR

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

AU - Gasteren, van, A.J.M.

AU - Tel, G.

PY - 1990

Y1 - 1990

N2 - 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.

AB - 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.

U2 - 10.1016/0020-0190(90)90027-U

DO - 10.1016/0020-0190(90)90027-U

M3 - Article

VL - 35

SP - 277

EP - 279

JO - Information Processing Letters

JF - Information Processing Letters

SN - 0020-0190

IS - 6

ER -