Mechanical translation of set theoretic problem specifications into efficient RAM code — A case study

Abstract

There have been various proposals for program development methodologies in which a computer system is used to aid in the formulation of precise problem specifications, in the synthesis of efficient and correct programs, and in the analysis of performance. A few systems have actually been implemented. Although some of these systems are fully general in expressive power, they all lack a sufficient degree of automation to make them viable alternatives to conventional ad hoc approaches. This paper illustrates a radically different, fully automatic top-down approach to program development in which formal problem specifications are mechanically translated into efficient RAM code. This code is guaranteed to be totally correct and its asymptotic running time is automatically determined. The user is only required to supply the system with a formal problem specification, and is relieved of major responsibilities in the rest of the program development process. These sharp results are obtained, in part, by restricting the system to handle a class of determinate, set theoretic, tractable problems. Most of the techniques described in this paper have been implemented and used effectively in the RAPTS transformational programming system. This paper explains the conceptual underpinnings of our approach by considering the problem of attribute closure for relational databases and systematically deriving a program that implements a solution.