18th Annual Symposium on Foundations of Computer Science (sfcs 1977) (1977)
Sept. 30, 1977 to Oct. 31, 1977
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/SFCS.1977.25
We argue that relative soundness and completeness theorems for Floyd-Hoare Axiom Systems (, , ) 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.
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.