Flow of control in the proof theory of structured programming
- 1 October 1975
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- No. 02725428,p. 29-33
- https://doi.org/10.1109/sfcs.1975.15
Abstract
The proof theory of structured programming insofar as concerned with flow of control is investigated. Various proof rules for the while, repeat-until and simple iteration statements - all essentially variants of Hoare's original while rule - are analyzed with respect to their soundness and adequacy. Next, a recently proposed proof rule for recursive procedures due to Dijkstra is - after correction - shown to be a simple instance of Scott's induction rule. Finally, Manna & Pnueli's rule for total correctness of the while statement is formally justified using the Hitchcock & Park theory of program termination based on well-founded relations.Keywords
This publication has 9 references indexed in Scilit:
- Least fixed points revisitedTheoretical Computer Science, 1976
- Structured Programming with go to StatementsACM Computing Surveys, 1974
- On the Composition of Well-Structured ProgramsACM Computing Surveys, 1974
- An axiomatic definition of the programming language PASCALPublished by Springer Nature ,1974
- A simple axiomatic basis for programming language constructsIndagationes Mathematicae, 1974
- An axiomatic definition of the programming language PASCALActa Informatica, 1973
- Fixpoint approach to the theory of computationCommunications of the ACM, 1972
- Procedures and parameters: An axiomatic approachLecture Notes in Mathematics, 1971
- An axiomatic basis for computer programmingCommunications of the ACM, 1969