# Accession Number:

## ADA275260

# Title:

## Program Derivation by Proof Transformation

# Descriptive Note:

## Doctoral thesis

# Corporate Author:

## CARNEGIE-MELLON UNIV PITTSBURGH PA DEPT OF COMPUTER SCIENCE

# Personal Author(s):

# Report Date:

## 1993-10-01

# Pagination or Media Count:

## 188.0

# 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 developers 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.

# Descriptors:

# Subject Categories:

- Operations Research
- Computer Programming and Software