PC-compactness, a necessary condition for the existence of sound and complete logics of partial correctness
Jan Aldert Bergstra, Jerzy Tiuryn · Centrum Wiskunde & Informatica (CWI), the national research institute for mathematics and computer science in the Netherlands · 1983
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.