Max-Planck-Institut für Informatik
max planck institut
informatik
mpii logo Minerva of the Max Planck Society
 

MPI-I-94-238

Formal methods of automated program improvement

Madden, Peter

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
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.
Acknowledgement:
References to related material:
Article: Database 'MPII AG2 Publications', View '1. Author/Editor \ 2. by Group', Document 'Recursive Program Optimization Through Inductive Synthesis Proof Transformation'

To download this research report, please select the type of document that fits best your needs.Attachement Size(s):
MPI-I-94-238.pdfMPI-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
Hide details for BibTeXBibTeX
@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},
}