Intellektik: Technical report 93-03
Metasynthesis -- Deriving Programs that Develop Programs, (Habilitationsschrift)
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.