PC-compactness, a necessary condition for the existence of sound and complete logics of partial correctness
A first order theory is called PC-compact if each asserted program which is true in all models of the theory is true in all models of a finite subset of the theory. If a structure has a complete Hoare's logic then its first order theory must be PC-compact; moreover, its partial correctness theory must be decidable relative to this first order theory.
This identifies two necessary conditions that a structure must satisfy if Hoare's logic (or any sound logic of partial correctness extending Hoare's logic) is to be complete on the given structure. We provide an example of a structure that satisfies both conditions, on which Hoare's logic is incomplete but which does possess a sound and complete logic of partial correctness. This logic is obtained by adding a proof rule which incorporates aprogram transformation. The concept of PC-compactness is further studied in detail by means of an examination of various example structures.
Key words & phrasesHoare's logic logic of partial correctness soundness completeness PC-compactness
Unable to display preview. Download preview PDF.
- BERGSTRA, J.A., A. CHMIELIENSKA & J. TIURYN, Hoare's logic is incomplete when it does not have to be, in Logics of Programs Ed. D. Kozen SpR. L.N.C.S. 131 (1981), 9–23.Google Scholar
- BERGSTRA, J.A. & J.V. TUCKER, Hoare's logic for programming languages with two datatypes, Math. Centre Department of Computer Science Technical Report IW 207 Amsterdam 1982.Google Scholar
- BERGSTRA, J.A. & J.V. TUCKER, Expressiveness and the completeness of Hoare's logic, JCSS, vol. 25, Nr. 3 (1983), p. 267–284.Google Scholar
- CHANG, C.C. & H.J. KEISLER, Model Theory, North Holland, Studies in logic vol. 73.Google Scholar
- COOK, S.A., Soundness and completeness of an axiom system for program verification, SIAM J. Computing 7 (1978), 70–90.Google Scholar
- HOARE, C.A.R., An axiomatic basis for computer programming, Communications ACM 12 (1967), 567–580.Google Scholar
- LAMBEK, J., How to program an infinite abacus, Canadian Mathematical Bulletin 4 (1961), 295–302.Google Scholar
- SHOENFIELD, J., Mathematical logic, Reading, Addison-Wesley (1967).Google Scholar
- WAND, M., A new incompleteness result for Hoare's system, J. Association Computing Machinary, 25 (1978), 168–175.Google Scholar