Program Derivation by Proof Transformation
Abstract
In the proofs-as-programs methodology, verified programs are developed through theorem-proving a constructive logic. Under this approach, the theorem-proving process can be regarded as a program derivation process. The merits of this approach to programming are twofold. First, working with proofs instead of programs concentrates the developer's effort on the intellectually difficult part of the development process: understanding, solving, and explaining the solution to a mathematical problem. Second, the proof provides a formal and trustworthy basis for an explanation of the program. This thesis investigates the use of proof transformation as a way to address important concerns in program derivation that are not addressed by theorem-proving alone. One difficulty with the proofs-as-programs strategy arises from the conflict between elegance and efficiency. A simple, elegant proof may lead to an inefficient program. A more complex proof that corresponds to a more efficient program may be difficult to invent or understand. With proof transformations, a developer can start with an elegant proof that is easy to understand, and incrementally derive a more complex proof and thus a more efficient program. Another problem comes from the need for adaptation and reuse. With current automated support for theorem-proving, it is difficult to re-use previous work other than by re-using lemmas from a library. This kind of reuse is analogous to the use of subroutine libraries in ordinary programming, and does not directly, support adaptation. Proof transformations provide a way of adapting a proof to a new context.
Document Details
- Document Type
- Technical Report
- Publication Date
- Oct 01, 1993
- Accession Number
- ADA275260
Entities
People
- Penny Anderson
Organizations
- Carnegie Mellon University