The Classical Methods of Floyd

Two proof methods for the verification of flowchart programs will now be introduced: the inductive assertions method and the well-founded sets method. The former method applies to proofs of partial correctness, the latter to proofs of termination. These proof methods capture the essence of the reasoning used in Example 6.8 (in the case of the inductive assertions method) and Example 6.9 (in the case of the well-founded sets method). Their improvement on the ad hoc reasoning lies in the use of predicate logic which leads to more elegant notation and in that some routine proof steps are filtered out.