de.mpg.escidoc.pubman.appbase.FacesBean
English

# Item

ITEM ACTIONSEXPORT

Released

Report

#### Formal methods of automated program improvement

##### MPS-Authors
http://pubman.mpdl.mpg.de/cone/persons/resource/persons44961

Programming Logics, MPI for Informatics, Max Planck Society;

##### Locator
There are no locators available
##### Fulltext (public)

MPI-I-94-238.pdf
(Any fulltext), 29MB

##### Supplementary Material (public)
There is no public supplementary material available
##### Citation

Madden, P. ().(1994). Formal methods of automated program improvement (MPI-I-94-238). Saarbrücken: Max-Planck-Institut für Informatik.

Cite as: http://hdl.handle.net/11858/00-001M-0000-0014-B7B9-C
##### Abstract
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.