This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
16th Annual Symposium on Foundations of Computer Science (FOCS 1975)
Flow of control in the proof theory of structured programming
October 13-October 15
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.
Citation:
J. W. de Bakker, "Flow of control in the proof theory of structured programming," focs, pp.29-33, 16th Annual Symposium on Foundations of Computer Science (FOCS 1975), 1975
Usage of this product signifies your acceptance of the Terms of Use.