Title

Program Derivation by Fixed Point Computation

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.

Department(s)

Mathematics and Statistics

Document Type

Article - Journal

Document Version

Citation

File Type

text

Language(s)

English

Rights

© 1989 Elsevier, All rights reserved.


Share

 
COinS