Subgoal induction

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.

REFERENCES

• 1: Basu, S., and Misra, J. Proving loop programs. IEEE Trans. Software Eng. SE-1, 1 (March 1975), 76-86.
• 2: Robert S. Boyer , J. Strother Moore, Proving Theorems about LISP Functions, Journal of the ACM (JACM), v.22 n.1, p.129-144, Jan. 1975 [doi>10.1145/321864.321875]
• 3: Burstall, R.M. Proving properties of programs by structural induction. Computer J. 12, 1 (Feb. 1969), 41-48.
• 4: Floyd, R.W. Assigning meanings to programs. Moth. Aspects of Computer Science, J.T. Schwartz, Ed., Amer. Math. Soc., Providence, R.I., 1967, pp. 19-32.
• 5: German, S.M., and Wegbreit, B. A synthesizer of inductive assertions. IEEE Trans. Software Eng., SE-1, 1 (March 1975), 68-75.
• 6: Donald I. Good , Ralph L. London , W. W. Bledsoe, An interactive program verification system, Proceedings of the international conference on Reliable software, p.482-492, April 21-23, 1975, Los Angeles, California
• 7: Hoare, C.A.R. Procedures and parameters: an axiomatic approach. Lecture Notes in Mathematics 188, E. Engeler, Ed., Springer-Verlag, 1971.
• 8: Shigeru Igarashi , Ralph L. London , David C. Luckham, Automatic program verification I: a logical basis and its implementation., Stanford University, Stanford, CA, 1973
• 9: McCarthy, J. A basis for a mathematical theory of computation. In Computer Programming and Formal Systems, P. Braffort and D.S. Hirschberg, Eds., North-Holland, Amsterdam, 1963, pp. 33-70.
• 10: McCarthy, J. and Painter, J.A. Correctness of a compiler for arithmetic expressions. Mathematical Aspects of Computer Science, J.T. Schwartz, Ed., Amer. Math. Sot., Providence, R.I., 1967, pp. 33-41.
• 11: Zohar Manna , Amir Pnueli, Formalization of Properties of Functional Programs, Journal of the ACM (JACM), v.17 n.3, p.555-569, July 1970 [doi>10.1145/321592.321606]
• 12: Zohar Manna , Stephen Ness , Jean Vuillemin, Inductive methods for proving properties of programs, Communications of the ACM, v.16 n.8, p.491-502, Aug. 1973 [doi>10.1145/355609.362336]
• 13: Zohar Manna, Introduction to Mathematical Theory of Computation, McGraw-Hill, Inc., New York, NY, 1974
• 14: Harlan D. Mills, The new math of computer programming, Communications of the ACM, v.18 n.1, p.43-48, Jan. 1975 [doi>10.1145/360569.360659]
• 15: Robin Milner, Implementation and applications of Scott's logic for computable functions, Proceedings of ACM conference on Proving assertions about programs, p.1-6, January 06-07, 1972, Las Cruces, New Mexico, United States
• 16: Moore, J.S. Introducing prog into the pure lisp theorem prover. CSL-74-3, Xerox Palo Alto Res. Center, Palo Alto, Calif. (Dec. 1974).
• 17: Topor, R.W. Interactive program verification using virtual programs. Ph.D. Th., University Of Edinburgh, Edinburgh, 1975.
• 18: Waldinger, R.J., and Levitt, K.N. Reasoning about programs. Artificial Intelligence 5, 3 (Fall 1974), 235-316.
• 19: Wegbreit, B. Complexity of synthesizing inductive assertions. Comptr. Sci. Lab., Xerox Palo Alto Res. Center, Palo Alto, Calif., Jan. 1975.
• 20: Manna, Z. Mathematical theory of partial correctness. J. Computer System Sci. 5, 3 (June 1971), 239-253.

INDEX TERMS

Keywords:
computation induction, induction rule, inductive assertions, iterative programs, program verification, proof rule, proving programs correct, recursive programs, structural induction