A Tutorial on Synthesis of Logic Programs from Specifications

Kung-Kiu Lau
Department of Computer Science, University of Manchester
Oxford Road, Manchester M13 9PL, United Kingdom
kung-kiu@cs.man.ac.uk

Geraint Wiggins
Department of Artificial Intelligence, University of Edinburgh
80 South Bridge, Edinburgh EH1 1HN, Scotland
geraint@aisb.ed.ac.uk

Abstract:
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 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, Hansson, Hogger, and Tarnlund. 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 was
rekindled, this time with a firm emphasis on automated or
semi-automated synthesis. Now there is an annual international workshop
on logic program synthesis and transformation.

The tutorial is organised as follows. We shall first define the basic concepts.
Then we shall describe a taxonomy of logic program synthesis
methods. For the main approaches in the taxonomy, we shall give
examples, with a view to illustrating the approaches as well as
comparing them.