Home Table of Contents News Blogs Opinion Research Practice Contributed Articles Review Articles Careers Archive Videos About Communications
Sign In
advertisement

Home → Magazine Archive → April 1977 (Vol. 20, No. 4) → Subgoal induction → Abstract

Subgoal induction

By James H. Morris, Ben Wegbreit

Communications of the ACM, Vol. 20 No. 4, Pages 209-222
10.1145/359461.359466

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.

The full text of this article is premium content

0 Comments

No entries found