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

\bibitem{CousotCousot87-AI}
P{.} Cousot and R{.} Cousot.
\newblock Sometime = Always + Recursion $\equiv$ Always, On the Equivalence
          of the Intermittent and Invariant Assertions Methods for Proving
          Inevitability Properties of Programs.
\newblock Acta Informatica 24, 1--31 (1987).

@article{CousotCousotCousot87-AI,
   author =    {Cousot, P{.} and Cousot, R{.}},
   title =     {Sometime = Always + Recursion $\equiv$ Always, On the Equivalence
               of the Intermittent and Invariant Assertions Methods for Proving
               Inevitability Properties of Programs},
   journal =   {Acta Informatica},
   volume =    24,
   pages =     {1--31},
   year =      {1987},
}

\bibitem{CousotR-TheseEtat-1985}
R. Cousot.
\newblock Fon\-de\-ments des m{\'e}\-tho\-des de preu\-ve d'in\-va\-rian\-ce et de
          fa\-ta\-li\-t{\'e} de pro\-gramm\-es pa\-ral\-l{\`e}\-les (in {F}rench).
\newblock Th{\`e}\-se d'{{\'E}}tat {\`e}s sci\-en\-ces ma\-th{\'e}\-ma\-ti\-ques,
          Ins\-ti\-tut Na\-tio\-nal Po\-ly\-tech\-ni\-que de Lor\-rai\-ne, Nan\-cy, 
          Fran\-ce, 15 November 1985.