Previous: TR 93-02 Next: TR 93-06


Intellektik: Technical report 93-03

Metasynthesis -- Deriving Programs that Develop Programs, (Habilitationsschrift)

Christoph Kreitz

The origins of this work go back to research on building systems for the automatic synthesis of programs from specifications, extending the capabilities of existing ones, making several systems cooperate, and integrating them into a larger programming environment. The experiences were rather frustrating. Program synthesis systems tend to be ad hoc implementations rather than being built systematically and well structured. It is not surprising that they have the same problems as other software products: there are all kinds of unexpected bugs, maintanance andmodifications become increasingly difficult, and cooperation with other synthesizers is nearly impossible despite of the fact that ideas behind the synthesis strategies show many similarities if explained verbally.

Apart from human shortcomings the main reason for this problem lies in a lack offormality in the steps from describing an idea on paper to its realization on a computer. Such formality, however, is difficult to achieve, extremely time consuming, and slows down the initial progress of a synthesis system. This is a price which many scientists are not willing to pay. On the other hand, the insufficiencies of current ``ad hoc'' systems are hardly acceptable --- and there are no exceptions --- and there is a need for tools supporting the systematic and formal development of program synthesis systems.

During the past years I have begun elaborating the theoretical foundations for such tools by formalizing the meta-theory of program development. The goal was to provide a theory which is both formally precise (to admit an immediate realization of concepts expressed in the theory on a computer) and uses a sufficently high level of abstraction (to make it humanly comprehensible and practically useful). I believe that such a theory will be a major step towards closing the gap between formal and informal reasoning in program synthesis and help overcoming problems like the ones mentioned above.

This paper presents the result of these investigations.

Full Paper: Compressed postscript Compressed DVI

BibTeX entry