Subgoal induction
- 1 April 1977
- journal article
- Published by Association for Computing Machinery (ACM) in Communications of the ACM
- Vol. 20 (4) , 209-222
- https://doi.org/10.1145/359461.359466
Abstract
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 step of a proof by subgoal induction to be valid.Keywords
This publication has 11 references indexed in Scilit:
- Proving loop programsIEEE Transactions on Software Engineering, 1975
- An interactive program verification systemPublished by Association for Computing Machinery (ACM) ,1975
- The new math of computer programmingCommunications of the ACM, 1975
- Proving Theorems about LISP FunctionsJournal of the ACM, 1975
- Reasoning about programsArtificial Intelligence, 1974
- Inductive methods for proving properties of programsCommunications of the ACM, 1973
- Implementation and applications of Scott's logic for computable functionsPublished by Association for Computing Machinery (ACM) ,1972
- Mathematical theory of partial correctnessJournal of Computer and System Sciences, 1971
- Formalization of Properties of Functional ProgramsJournal of the ACM, 1970
- Proving Properties of Programs by Structural InductionThe Computer Journal, 1969