18th Annual Symposium on Foundations of Computer Science (sfcs 1977) (1977)

Sept. 30, 1977 to Oct. 31, 1977

ISSN: 0272-5428

pp: 18-29

DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/SFCS.1977.25

ABSTRACT

We argue that relative soundness and completeness theorems for Floyd-Hoare Axiom Systems ([6], [5], [18]) are really fixed point theorems. We give a characterization of program invariants as fixed points of functionals which may be obtained in a natural manner from the text of a program. We show that within the framework of this fixed point theory, relative soundness and completeness results have a particularly simple interpretation. Completeness of a Floyd-Hoare Axiom system is equivalent to the existence of a fixed point for an appropriate functional, and soundness follows from the maximality of this fixed point, The functionals associated with regular procedure declarations are similar to predicate transformers of Dijkstra; for non-regular recursions it is necessary to use a generalization of the predicate transformer concept which we call a relational transformer.

INDEX TERMS

CITATION

E. M. Clarke, "Program invariants as fixed points,"

*18th Annual Symposium on Foundations of Computer Science (sfcs 1977)(FOCS)*, vol. 00, no. , pp. 18-29, 1977.

doi:10.1109/SFCS.1977.25

CITATIONS