Induction in Proofs about Programs.
Abstract
Four methods for proving equivalence of programs by induction are described and compared. They are recursion induction, structural induction, micro-rule induction, and truncation induction. McCarthy's formalism for conditional expressions as function definitions is used and reinterpreted in view of Park's work on results in lattice theory as related to proofs about programs. The possible application of this work to automatic program verification is discussed. (Author)
Document Details
- Document Type
- Technical Report
- Publication Date
- Feb 01, 1972
- Accession Number
- AD0737701
Entities
People
- Irene G. Greif
Organizations
- Massachusetts Institute of Technology