Forms of Logic Specifications: A Preliminary Study

Kung-Kiu Lau
Department of Computer Science
University of Manchester
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:
There is no universal agreement on exactly what form a
specification should take, what part it should play in synthesis, and
what its precise relationship with the specified program should be.
In logic programming, the role of specification is all the more 
unclear since logic programs are often used as executable 
specifications. In this paper we take the view that specifications
should be set in the context of the problem domain, which we call a
framework. We conduct a preliminary study of two useful forms of logic
specifications: if-and-only-if and partial specifications. First we
set up a three-tier formalism for synthesis, the top-tier being a
framework. Then within this formalism we define these two
forms of specifications, and discuss their roles in synthesis.