max planck institut
informatik

# MPI-I-94-238

## Formal methods of automated program improvement

MPI-I-94-238. August 1994, 12 pages. | Status: available - back from printing | Next --> Entry | Previous <-- Entry

Abstract in LaTeX format:
Systems supporting the manipulation of non-trivial program code are
complex and are at best semi-automatic. However, formal methods, and
in particular theorem proving, are providing a growing foundation of
techniques for automatic program development (synthesis, improvement,
transformation and verification). In this paper we report on novel
research concerning: (1) the exploitation of synthesis proofs for the
purposes of automatic program optimization by the transformation of
proofs, and; (2) the automatic synthesis of efficient programs from
standard equational definitions. A fundamental theme exhibited by our
research is that mechanical program construction, whether by direct
synthesis or transformation, is tantamount to program verification
plus higher-order reasoning. The exploitation of the
over more traditional approaches to program improvement. For example,
we are able to automate the identification of efficient recursive
data-types which usually correspond to {\em eureka} steps in pure''
transformational techniques such as unfold/fold. Furthermore, all
transformed, and synthesized, programs are guaranteed correct with
respect to their specifications.
Acknowledgement:
References to related material:
Article:

MPI-I-94-238.pdf29107 KBytes
Please note: If you don't have a viewer for PostScript on your platform, try to install GhostScript and GhostView

URL to this document: http://domino.mpi-inf.mpg.de/internet/reports.nsf/NumberView/1994-238
BibTeX