Relative completeness of a Hoare-calculus for while-programs

In several papers,e.g. [COOK] or [APT] the problems of correctness and completeness of Hoare calculi have been studied. The purpose of this paper is to present a simple approach to this subject by restricting the attention to a very small class of programs, the so-called while-programs.- 1-1. Preliminaries As Hoare logic is an extension of first order predicate logic. a few definitions and notations of mathematical logic are shortly recalled: A first order predicate language t is built up from a basis B = (.E. p. V). where F is a set of function symbols; with each element of F is associated an integer k ~ O. called its arity P is a set of predicate symbols; with each element of P i