Program Derivation by Fixed Point Computation

Author

Jiazhen Cai
Robert Paige L., Missouri University of Science and TechnologyFollow

Abstract

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.

Recommended Citation

J. Cai and R. Paige, "Program Derivation by Fixed Point Computation," Science of Computer Programming, Elsevier, Jan 1989.

The definitive version is available at https://doi.org/10.1016/0167-6423(88)90033-0

Department(s)

Mathematics and Statistics

International Standard Serial Number (ISSN)

0167-6423

Document Type

Article - Journal

Document Version

Citation

File Type

text

Language(s)

English

Rights

© 1989 Elsevier, All rights reserved.

Publication Date

01 Jan 1989