On Specification Frameworks and Deductive Synthesis of Logic Programs Kung-Kiu Lau Department of Computer Science, University of Manchester Oxford Road, Manchester M13 9PL, United Kingdom kung-kiu@cs.man.ac.uk Mario Ornaghi Dipartimento di Scienze dell'Informazione Universita' degli studi di Milano Via Comelico 39/41, Milano, Italy ornaghi@dsi.unimi.it Abstract: Logic program synthesis methods can be roughly divided into those that use a formal specification and a formal synthesis process, and those that use an informal specification and an informal synthesis technique. In formal methods for logic program synthesis, the issue of what specification language is best has never loomed large, because first-order logic is the obvious candidate and hence the natural choice. This, in our view, has resulted in an over-simplistic view of logic program specifications. In our own area of deductive synthesis of logic programs, for example, a specification is often just an if-and-only-if first-order definition, or a set of such definitions. Such a simplistic approach to specification has, in our experience, two major drawbacks: - It cannot capture the entire body of knowledge needed for and used in the synthesis process. - It does not provide an adequate means to specify properties other than correctness. In our work, therefore, we have used specification frameworks to provide the background for deductive synthesis of logic programs. In this paper, we take a closer look at such frameworks. We shall explain what they are, and how they can be used to specify properties such as correctness and modularity (and hence reusability). Moreover, we shall show that there is a close two-way relationship between specification frameworks and deductive synthesis. In particular, a deductive synthesis process can provide a useful feedback mechanism which can not only check for desirable properties in the specification framework, but also improve the framework (with regard to such properties) using the result of the synthesis.