Inductive methods for proving properties of programs
- 1 August 1973
- journal article
- Published by Association for Computing Machinery (ACM) in Communications of the ACM
- Vol. 16 (8), 491-502
- https://doi.org/10.1145/355609.362336
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 7 references indexed in Scilit:
- Fixpoint approach to the theory of computationCommunications of the ACM, 1972
- Implementation and applications of Scott's logic for computable functionsPublished by Association for Computing Machinery (ACM) ,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 expressionsProceedings of Symposia in Applied Mathematics, 1967
- Assigning meanings to programsProceedings of Symposia in Applied Mathematics, 1967