Logic of Programs 1983: Logics of Programs pp 45-56

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

• J. A. Bergstra
• J. Tiuryn
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 164)

## 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

## References

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