Access Restriction

Author Wegbreit, Ben ♦ Morris, James H.
Source ACM Digital Library
Content type Text
Publisher Association for Computing Machinery (ACM)
File Format PDF
Language English
Subject Keyword Induction rule ♦ Proof rule ♦ Computation induction ♦ Structural induction ♦ Inductive assertions ♦ Proving programs correct ♦ Iterative programs ♦ Program verification ♦ Recursive programs
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.
Description Affiliation: Xerox Palo Alto Research Center, Palo Alto, CA (Morris, James H.; Wegbreit, Ben)
Age Range 18 to 22 years ♦ above 22 year
Educational Use Research
Education Level UG and PG
Learning Resource Type Article
Publisher Date 2005-08-01
Publisher Place New York
Journal Communications of the ACM (CACM)
Volume Number 20
Issue Number 4
Page Count 14
Starting Page 209
Ending Page 222

Open content in new tab

   Open content in new tab
Source: ACM Digital Library