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.