Program Derivation by Fixed Point Computation
This paper develops a transformational paradigm by which nonnumerical algorithms are treated as fixed point computations derived from very high level problem specifications. We begin by presenting an abstract functional problem specification language SQ+, which is shown to express any partial recursive function in a fixed point normal form. Next, we give a nondeterministic iterative schema that in the case of finite iteration generalizes the "chaotic iteration” of Cousot and Cousot for computing fixed points of monotone functions efficiently. New techniques are discussed for recomputing fixed points of distributive functions efficiently. Numerous examples illustrate how these techniques for computing and recomputing fixed points can be incorporated within a transformational programming methodology to facilitate the design and verification of nonnumerical algorithms.
J. Cai and R. Paige, "Program Derivation by Fixed Point Computation," Science of Computer Programming, Elsevier, Jan 1989.
The definitive version is available at http://dx.doi.org/10.1016/0167-6423(88)90033-0
Mathematics and Statistics
Article - Journal
© 1989 Elsevier, All rights reserved.