A Comparative Analysis of Functional Correctness

Abstract

The functional correctness technique is presented and discussed. It is also explained that the underlying theory has an implicatmn for the derivation of loop invariants. The functional verification conditions concerning program loops are then shown to be a specialization of the commonly used inductive assertion verification conditions. Next, the functional technique is compared and contrasted with subgoal induction. Finally, the difficulty of proving initialized loop programs is examined in light of both the inductive assertion and functional correctness theories. © 1982, ACM. All rights reserved.