A New Incompleteness Result for Hoare's System
Mitchell Wand · Journal of the ACM · 1978
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 discussed