| The use of modules to decompose large software systems into smaller, more manageable, programming tasks is now widely accepted. To benefit from such a decomposition, the requirements of each module have to be defined in a module interface specification. The modules must then be implemented according to their specifications. We propose a method for deriving Prolog implementations of modules by transforming interface specifications written in logic.;We present the scSCS method for writing module interface specifications in logic. With this method we obtain precision in both syntax and semantics. By using logic, we satisfy the standard criterion for semantic precision: statements about a module's externally observable behaviour are logical consequences of the specification, when regarded as a theory of first-order logic. The specifications can be written so that they are executable as Prolog programs.;Although the specifications are executable, they are often inefficient. Logic-based program transformation allows us to make a logic program more efficient while preserving its meaning. We present a method for specializing a program for a particular query using a "complete set of frontiers." This idea is incorporated into scFROST, an interactive transformation system that assists the user with the construction of complete sets of frontiers.;Finally, we show how we can transform an scSCS specification so that it can serve as an implementation. Although part of this transformation can be applied systematically, we cannot derive the entire implementation for even the simplest modules. We discuss the problems that occur and look at alternatives for obtaining confidence in the correctness of an implementation. |
