A Tutorial on Synthesis of Logic Programs from Specifications

1 Introduction Program synthesis is concerned with deriving programs from their specifications. Such specifications (and corresponding derivations) may be formal or informal . Formal methods have an advantage over informal ones, in that they have the desirable 1 property of being able to formally prove the correctness of the derived programs. Logic programming provides a uniquely uniform framework for specifications, programs and program synthesis. It is small wonder that in the early days of logic programming, program synthesis was one of the first topics that received attention. Most notable among this early work is that of Clark [2], Hansson [4], Hogger [6], and Tarnlund [5]. Although Hansson and Tarnlund and their colleagues at Uppsala implemented a derivation editor, the early work was not particularly geared towards automated synthesis. For some reason, work on logic program synthesis dwindled considerably in the Eighties. However, at the beginning of the Nineties, interest w..