hide
Free keywords:
-
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.
