Inductive methods for proving properties of programs
Authors:
Open Access
- 1 August 1973
- journal article
- Published by Association for Computing Machinery (ACM) in Communications of the ACM
- Vol. 16 (8) , 491-502
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.Keywords
This publication has 8 references indexed in Scilit:
- Fixpoint approach to the theory of computationCommunications of the ACM, 1972
- Implementation and applications of Scott's logic for computable functions1972
- Recursive definitions of partial functions and their computationsACM SIGACT News, 1972
- Another recursion induction principleCommunications of the ACM, 1971
- Formalization of Properties of Functional ProgramsJournal of the ACM, 1970
- Proving Properties of Programs by Structural InductionThe Computer Journal, 1969
- Correctness of a compiler for arithmetic expressions1967
- Assigning meanings to programs1967