‘A la Floyd’ induction principles for proving inevitability properties of programs.
In «Algebraic methods in semantics», M. Nivat and J. Reynolds (Eds.), Cambridge University Press, Cambridge, UK, pp. 277—312, December 1985.
When the behavior of the transition system is specified by a non-closed set of execution traces (e.g. fair parallelism), Floyd's computational induction method cannot be applied without auxiliary variables. One approach consists in using Floyd's method for an auxiliary transition relation on states and history variables that exactly generates the original set of traces. Another approach consists in a generalization of the use of loop cutpoints in Floyd's method, in that the choice of the cutpoints (where some termination function has to be decreased) may depend upon computation histories cumulated into auxiliary variables.
\bibitem{CousotCousot85-AMS}
P{.} Cousot and R{.} Cousot.
\newblock 'A la Floyd' induction principles for proving inevitability
properties of programs.
\newblock In \emph{Algebraic methods in semantics}, M{.} Nivat and J{.}
Reynolds (Eds.), Cambridge University Press, Cambridge, UK , pp{.}
277--312, December 1985.
@inproceedings{CousotCousot85-AMS,
author = {Cousot, P{.} and Cousot, R{.}},
title = {'A la Floyd' induction principles for proving inevitability
properties of programs},
booktitle = {Algebraic methods in semantics},
editor = {M{.} Nivat and J{.} Reynolds},
publisher = {Cambridge University Press, Cambridge, UK},
pages = {277--312},
month = dec,
year = {1985},
}
)
\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.