Sometime = always + recursion ≡ always on the equivalence of the intermittent and invariant assertions methods for proving inevitability properties of programs

Patrick Cousot, Radhia Cousot

Research output: Contribution to journalArticle

Abstract

We propose and compare two induction principles called "always" and "sometime" for proving inevitability properties of programs. They are respective formalizations and generalizations of Floyd invariant assertions and Burstall intermittent assertions methods for proving total correctness of sequential programs whose methodological advantages or disadvantages have been discussed in a number of previous papers. Both principles are formalized in the abstract setting of arbitrary nondeterministic transition systems and illustrated by appropriate examples. The "sometime" method is interpreted as a recursive application of the "always" method. Hence "always" can be considered as a special case of "sometime". These proof methods are strongly equivalent in the sense that a proof by one induction principle can be rewritten into a proof by the other one. The first two theorems of the paper show that an invariant for the "always" method can be translated into an invariant for the "sometime" method even if every recursive application of the later is required to be of finite length. The third and main theorem of the paper shows how to translate an invariant for the "sometime" method into an invariant for the "always" method. It is emphasized that this translation technique follows the idea of transforming recursive programs into iterative ones. Of course, a general translation technique does not imply that the original "sometime" invariant and the resulting "always" invariant are equally understandable. This is illustrated by an example.

Original languageEnglish (US)
Pages (from-to)1-31
Number of pages31
JournalActa Informatica
Volume24
Issue number1
DOIs
StatePublished - Feb 1987

ASJC Scopus subject areas

  • Information Systems

Cite this

@article{ad62e3caffba49a2a0adfe5c59df1a1f,
title = "Sometime = always + recursion ≡ always on the equivalence of the intermittent and invariant assertions methods for proving inevitability properties of programs",
abstract = "We propose and compare two induction principles called {"}always{"} and {"}sometime{"} for proving inevitability properties of programs. They are respective formalizations and generalizations of Floyd invariant assertions and Burstall intermittent assertions methods for proving total correctness of sequential programs whose methodological advantages or disadvantages have been discussed in a number of previous papers. Both principles are formalized in the abstract setting of arbitrary nondeterministic transition systems and illustrated by appropriate examples. The {"}sometime{"} method is interpreted as a recursive application of the {"}always{"} method. Hence {"}always{"} can be considered as a special case of {"}sometime{"}. These proof methods are strongly equivalent in the sense that a proof by one induction principle can be rewritten into a proof by the other one. The first two theorems of the paper show that an invariant for the {"}always{"} method can be translated into an invariant for the {"}sometime{"} method even if every recursive application of the later is required to be of finite length. The third and main theorem of the paper shows how to translate an invariant for the {"}sometime{"} method into an invariant for the {"}always{"} method. It is emphasized that this translation technique follows the idea of transforming recursive programs into iterative ones. Of course, a general translation technique does not imply that the original {"}sometime{"} invariant and the resulting {"}always{"} invariant are equally understandable. This is illustrated by an example.",
author = "Patrick Cousot and Radhia Cousot",
year = "1987",
month = "2",
doi = "10.1007/BF00290704",
language = "English (US)",
volume = "24",
pages = "1--31",
journal = "Acta Informatica",
issn = "0001-5903",
publisher = "Springer New York",
number = "1",

}

TY - JOUR

T1 - Sometime = always + recursion ≡ always on the equivalence of the intermittent and invariant assertions methods for proving inevitability properties of programs

AU - Cousot, Patrick

AU - Cousot, Radhia

PY - 1987/2

Y1 - 1987/2

N2 - We propose and compare two induction principles called "always" and "sometime" for proving inevitability properties of programs. They are respective formalizations and generalizations of Floyd invariant assertions and Burstall intermittent assertions methods for proving total correctness of sequential programs whose methodological advantages or disadvantages have been discussed in a number of previous papers. Both principles are formalized in the abstract setting of arbitrary nondeterministic transition systems and illustrated by appropriate examples. The "sometime" method is interpreted as a recursive application of the "always" method. Hence "always" can be considered as a special case of "sometime". These proof methods are strongly equivalent in the sense that a proof by one induction principle can be rewritten into a proof by the other one. The first two theorems of the paper show that an invariant for the "always" method can be translated into an invariant for the "sometime" method even if every recursive application of the later is required to be of finite length. The third and main theorem of the paper shows how to translate an invariant for the "sometime" method into an invariant for the "always" method. It is emphasized that this translation technique follows the idea of transforming recursive programs into iterative ones. Of course, a general translation technique does not imply that the original "sometime" invariant and the resulting "always" invariant are equally understandable. This is illustrated by an example.

AB - We propose and compare two induction principles called "always" and "sometime" for proving inevitability properties of programs. They are respective formalizations and generalizations of Floyd invariant assertions and Burstall intermittent assertions methods for proving total correctness of sequential programs whose methodological advantages or disadvantages have been discussed in a number of previous papers. Both principles are formalized in the abstract setting of arbitrary nondeterministic transition systems and illustrated by appropriate examples. The "sometime" method is interpreted as a recursive application of the "always" method. Hence "always" can be considered as a special case of "sometime". These proof methods are strongly equivalent in the sense that a proof by one induction principle can be rewritten into a proof by the other one. The first two theorems of the paper show that an invariant for the "always" method can be translated into an invariant for the "sometime" method even if every recursive application of the later is required to be of finite length. The third and main theorem of the paper shows how to translate an invariant for the "sometime" method into an invariant for the "always" method. It is emphasized that this translation technique follows the idea of transforming recursive programs into iterative ones. Of course, a general translation technique does not imply that the original "sometime" invariant and the resulting "always" invariant are equally understandable. This is illustrated by an example.

UR - http://www.scopus.com/inward/record.url?scp=0023294103&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=0023294103&partnerID=8YFLogxK

U2 - 10.1007/BF00290704

DO - 10.1007/BF00290704

M3 - Article

AN - SCOPUS:0023294103

VL - 24

SP - 1

EP - 31

JO - Acta Informatica

JF - Acta Informatica

SN - 0001-5903

IS - 1

ER -