Inductive methods for proving properties of programs

ABSTRACT

There are two main purposes in this paper: first, clarification and extension of known results about computation of recursive programs, with emphasis on the difference between the theoretical and practical approaches; second, presentation and examination of various known methods for proving properties of recursive programs. Discussed in detail are two powerful inductive methods, computational induction and structural induction, including examples of their applications.

REFERENCES

• 1: Burstall, R.M. Proving properties of programs by structural induction. Computer J. 12, 1 (Feb. 1969), 41-48.
• 2: Jean-Marie Cadiou, Recursive definitions of partial functions and their computations, 1972
• 3: deBakker, J.W., and Scott, D. A theory of programs (unpublished memo., Aug. 1969).
• 4: Floyd, R.W. Assigning meanings to programs. Proc. Sympo. in Appl. Math. Vol. 19. Mathematical Aspects of Computer Science, (J.T. Schwartz, Ed.) AMS, Providence, R.I., 1967, pp. 19-32.
• 5: Grief, I.G. Induction in proofs about programs. Master's Th., M.I.T., 1972.
• 6: Kleene, S.C. Introduction to Metamathematics. D. Van Nostrand, Princeton, N.J., 1950.
• 7: 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]
• 8: Zohar Manna , Jean Vuillemin, Fixpoint approach to the theory of computation, Communications of the ACM, v.15 n.7, p.528-536, July 1972 [doi>10.1145/361454.361460]
• 9: McCarthy, John, and Painter, J.A. Correctness of a compiler for arithmetic expressions. Proc. Sympo. in Appl. Math. Vol. 19. Mathematical Aspects of Computer Science, (J.T. Schwartz, Ed.) AMS, Providence, RT, 1967, pp. 33-41.
• 10: Robin Milner, Logic for Computable Functions: description of a machine implementation., Stanford University, Stanford, CA, 1972
• 11: 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
• 12: Marvin Lee Minsky, Computation: Finite and Infinite Machines, Prentice-Hall, Inc., Upper Saddle River, NJ, 1967
• 13: Morris, James H. Lambda-calculus models of programming languages. Ph.D. Th., Proj. MAC, MIT, MAC-TR-57, Dec. 1968.
• 14: James H. Morris, Jr., Another recursion induction principle, Communications of the ACM, v.14 n.5, p.351-354, May 1971 [doi>10.1145/362588.362598]
• 15: Park, David. Fixpoint induction and proofs of program properties. In Machine Intelligence 5, (B. Meltzer and D. Miehie, Eds.) Edinburgh U. Press, Edinburgh, 1969, pp. 59-78.
• 16: Scott, Dana. Outline of a mathematical theory of computation. Proc. Fourth Ann. Princeton Conf. on Information Sciences and Systems, Princeton U., 1970, pp. 169-176.
• 17: Jean Etienne Vuillemin, Proof-techniques for recursive programs., 1974

INDEX TERMS

Keywords:
computational induction, least fixedpoint, recursive programs, structural induction