On Relative Completeness of Programming Logics

Abstract

In this paper a generalization of a certain Lipton's theorem (see Lipton [5]) is presented. Namely, we show that for a wide class of programming languages the following holds: the set of all partial correctness assertions true in an expressive interpretation I is uniformly decidable (in I) in the theory of I iff the halting problem is decidable for finite interpretations. In the effect we show that such limitations as effectiveness or Herbrand definability of interpretation (they are relevant in the previous proofs) can be removed in the case of partial correctness.