This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Consequence Verification of Flowcharts
January 1981 (vol. 7 no. 1)
pp. 52-60
K.L. Clark, Department of Computing and Control, Imperial College of Science and Technology
A common basis is presented, for Floyd's method of inductive assertions and for the subgoal induction method of Morris and Wegbreit. This basis is provided by consequence verification, a method for verifying logic programs. We connect flowcharts with logic programs by giving a recursive definition of the set of all computations of a flowchart. This definition can be given in two ways: the recursion can run forward or backward. Both definitions can be expressed in logic, resulting in a logic program which is then subjected to consequence verification. Verification of the forward logic program is shown to be essentially Floyd's method; verification of the backward program corresponds similarly to subgoal induction.
Index Terms:
subgoal induction, Consequence verification, inductive assertions, logic programming, program verification
Citation:
K.L. Clark, M.H. Van Emden, "Consequence Verification of Flowcharts," IEEE Transactions on Software Engineering, vol. 7, no. 1, pp. 52-60, Jan. 1981, doi:10.1109/TSE.1981.234508
Usage of this product signifies your acceptance of the Terms of Use.