The Community for Technology Leaders
18th Annual Symposium on Foundations of Computer Science (sfcs 1977) (1977)
Sept. 30, 1977 to Oct. 31, 1977
ISSN: 0272-5428
pp: 18-29
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
93 ms
(Ver 3.3 (11022016))