Inductive methods for proving properties of programs
Zohar Manna, Stephen Ness, Jean E. Vuillemin · Communications of the ACM · 1973
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.