Issue No. 01 - January (1981 vol. 7)
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.
subgoal induction, Consequence verification, inductive assertions, logic programming, program verification
K. Clark and M. Van Emden, "Consequence Verification of Flowcharts," in IEEE Transactions on Software Engineering, vol. 7, no. , pp. 52-60, 1981.