Developing Correct and Efficient Logic Programs by Transformation

The complex process of deriving programs from specifications is often divided into the following three steps: i) the derivation of formal specifications from the informal ones, ii) the validation of the formal specifications, and iii) the derivation of executable programs from the formal specifications. Each step of this derivation process can be supported by the use of elegant and well-understood notions of mathematical logic. In particular, from informal specifications given as sentences in a restricted form of the natural language, one can derive formal specifications as formulas of a first order logical theory [20]. One may then validate the derived formal specifications by checking whether or not they are consistent and satisfy some suitable properties. Finally, as we will illustrate in this paper, from formal specifications one may obtain executable, efficient programs by using techniques for transforming logic programs. This is, indeed, one of the reasons that makes logic programming very attractive for program construction. During this final step from specifications to programs, in order to improve efficiency one may want to use program transformation for avoiding multiple visits of data structures, or replacing complex forms of recursion by tail recursion, or reducing nondeterminism of procedures.