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)


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 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  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]
    SHOENFIELD, J., Mathematical logic, Reading, Addison-Wesley (1967).Google Scholar
  9. [9]
    WAND, M., A new incompleteness result for Hoare's system, J. Association Computing Machinary, 25 (1978), 168–175.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1984

Authors and Affiliations

  • J. A. Bergstra
    • 1
  • J. Tiuryn
    • 2
  1. 1.Mathematical CenterAmsterdamThe Netherlands
  2. 2.Institute of MathematicsUniversity of WarsawPoland

Personalised recommendations