### 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 language | English (US) |
---|---|

Pages (from-to) | 1-31 |

Number of pages | 31 |

Journal | Acta Informatica |

Volume | 24 |

Issue number | 1 |

DOIs | |

State | Published - Feb 1987 |

### ASJC Scopus subject areas

- Information Systems

### Cite this

**Sometime = always + recursion ≡ always on the equivalence of the intermittent and invariant assertions methods for proving inevitability properties of programs.** / Cousot, Patrick; Cousot, Radhia.

Research output: Contribution to journal › Article

}

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 -