``A la Burstall'' intermittent assertions induction principles for proving inevitability properties of programs (Q689297): Difference between revisions

The paper generalizes Burstall's (and that of Manna and Waldinger) intermittent assertions method to handle some properties of nondeterministic and parallel programs. Thus, as in operational semantics of programming languages, programs are modeled by transition systems, and program execution by complete traces. Termination and total correctness are modeled by inevitability properties, which are proved by Burstall's method and by some more abstract induction principles which generalise Burstall's method. The soundness, completeness and semantic completeness of this induction principle is proved. As the authors say, this study should be extended so as to take fairness hypotheses for parallel programs into account, and in order to obtain better presentations for logic programming.