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

A.J.M. Gasteren, van, G. Tel

Research output: Contribution to journalArticleAcademicpeer-review

6 Citations (Scopus)
3 Downloads (Pure)

Abstract

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.
Original languageEnglish
Pages (from-to)277-279
JournalInformation Processing Letters
Volume35
Issue number6
DOIs
Publication statusPublished - 1990

Fingerprint

Dive into the research topics of 'Comments on "On the proof of a distributed algorithm" : always-true is not invariant'. Together they form a unique fingerprint.

Cite this