de.mpg.escidoc.pubman.appbase.FacesBean
Deutsch

Hilfe Wegweiser Impressum Kontakt Einloggen

# Datensatz

DATENSATZ AKTIONENEXPORT

Freigegeben

Bericht

#### Formal methods of automated program improvement

##### MPG-Autoren
http://pubman.mpdl.mpg.de/cone/persons/resource/persons44961

Programming Logics, MPI for Informatics, Max Planck Society;

##### Externe Ressourcen
Es sind keine Externen Ressourcen verfügbar
##### Volltexte (frei zugänglich)

MPI-I-94-238.pdf
(beliebiger Volltext), 29MB

##### Ergänzendes Material (frei zugänglich)
Es sind keine frei zugänglichen Ergänzenden Materialien verfügbar
##### Zitation

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

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.