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