Subgoal Induction A proof method, subgoal induction, is presented as an alternative or supplement to the commonly used inductive assertion method. Its major virtue is that it can often be used to prove a loop's correctness directly from its input-output specification without the use of an invariant. The relation between subgoal induction and other commonly used induction rules is explored and, in particular, it is shown that subgoal induction can be viewed as a specialized form of computation induction. A set of sufficient conditions are presented which guarantee that an input-output specification is strong enough for the induction steps of a proof by subgoal induction to be valid. CACM April, 1977 Morris, J. H. Jr. Wegbreit, B. program verification, proving programs correct, induction rule, computation induction, inductive assertions, structural induction, proof rule, recursive programs, iterative programs 4.19 4.22 5.21 5.24 CA770401 JB December 29, 1977 6:31 AM 2981 4 2981 3030 4 2981 3077 4 2981 3104 4 2981 2457 5 2981 2981 5 2981 2981 5 2981 2981 5 2981 3014 5 2981 1834 6 2981 2981 6 2981