MPI-INF/SWS Research Reports 1991-2021

2. Number - All Departments


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

URL to this document:

Hide details for BibTeXBibTeX
  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},