Mechanical Translation of Set Theoretic Problem Specifications into Efficient Ram Code-a Case Study
Abstract
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.
Recommended Citation
R. Paige and F. Henglein, "Mechanical Translation of Set Theoretic Problem Specifications into Efficient Ram Code-a Case Study," Journal of Symbolic Computation, Elsevier, Jan 1987.
The definitive version is available at https://doi.org/10.1016/S0747-7171(87)80066-4
Department(s)
Mathematics and Statistics
International Standard Serial Number (ISSN)
0747-7171
Document Type
Article - Journal
Document Version
Citation
File Type
text
Language(s)
English
Rights
© 1987 Elsevier, All rights reserved.
Publication Date
01 Jan 1987
