# PC-compactness, a necessary condition for the existence of sound and complete logics of partial correctness

## Abstract

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 & phrases

Hoare's logic logic of partial correctness soundness completeness PC-compactness## Preview

Unable to display preview. Download preview PDF.

## References

- [1]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 - [2]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 - [3]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 - [4]CHANG, C.C. & H.J. KEISLER,
*Model Theory*, North Holland, Studies in logic vol. 73.Google Scholar - [5]COOK, S.A.,
*Soundness and completeness of an axiom system for program verification*, SIAM J. Computing 7 (1978), 70–90.Google Scholar - [6]HOARE, C.A.R.,
*An axiomatic basis for computer programming*, Communications ACM 12 (1967), 567–580.Google Scholar - [7]LAMBEK, J.,
*How to program an infinite abacus*, Canadian Mathematical Bulletin 4 (1961), 295–302.Google Scholar - [8]SHOENFIELD, J.,
*Mathematical logic*, Reading, Addison-Wesley (1967).Google Scholar - [9]WAND, M.,
*A new incompleteness result for Hoare's system*, J. Association Computing Machinary, 25 (1978), 168–175.Google Scholar