MPI-I-94-238
Formal methods of automated program improvement
Madden, Peter
August 1994, 12 pages.
.
Status: available - back from printing
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
proofs-as-programs paradigm lends our approach numerous advantages
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.
References to related material:
Article:
URL to this document: https://domino.mpi-inf.mpg.de/internet/reports.nsf/NumberView/1994-238
BibTeX
@TECHREPORT{Madden94-238,
AUTHOR = {Madden, Peter},
TITLE = {Formal methods of automated program improvement},
TYPE = {Research Report},
INSTITUTION = {Max-Planck-Institut f{\"u}r Informatik},
ADDRESS = {Im Stadtwald, D-66123 Saarbr{\"u}cken, Germany},
NUMBER = {MPI-I-94-238},
MONTH = {August},
YEAR = {1994},
ISSN = {0946-011X},
}