A New Incompleteness Result for Hoare's System
- 1 January 1978
- journal article
- Published by Association for Computing Machinery (ACM) in Journal of the ACM
- Vol. 25 (1) , 168-175
- https://doi.org/10.1145/322047.322062
Abstract
There exist structures for which Hoare's formal system for partial correctness is incomplete, even ff the entire first-order theory of the structure is included among the axioms This incompleteness occurs even if attention is restricted to structures with a solvable halting problem, and to programs which always halt on the structure The implications of this result for program proving are discussedKeywords
This publication has 4 references indexed in Scilit:
- On the completeness of the inductive assertion methodJournal of Computer and System Sciences, 1975
- Proving Theorems about LISP FunctionsJournal of the ACM, 1975
- Proof of a programCommunications of the ACM, 1971
- An axiomatic basis for computer programmingCommunications of the ACM, 1969