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

This paper illustrates a 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 an upper bound on its worst case asymptotic running time is automatically determined. The user is only required to supply the system with a formal problem specification, and is relieved of all responsibilities in the rest of the program development process. These results are obtained, in part, by greatly restricting the system to handle a class of determinate, set theoretic, tractable problems. The most essential transformational techniques that are used are fixed point iteration, finite differencing, and data structure selection. Rudimentary forms of these techniques 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 linear time solution