A Simple Proof for the Completeness of Floyd's Method
In [4], Csirmaz defined a semantics for programs, and proved the completeness of Floyd's method w.r.t, this semantics, generalizing the results in [2]. The semantics in [4] is the most natural generalization of the continuous traces semantics of [2]. The proof in [4] is rather deep and difficult, constructing counterexamples (models) for unprovable programs. Here we give a simple direct proof for this completeness result constructing the Floyd proofs themselves. The present proof is simpler than even the original proof in [2] which worked only for the special case of theories containing Peano arithmetic. The theorem in [4] turned out to be rather important in at least two branches of Nonstandard Dynamic Logic (NDL), namely in the 'lattice of program verification methods' and in the 'explicit representations of famous program verification methods' (see, e.g., [6, 7, 3, 1] or, for NDL in general, [5]). Thus, the rSle of the theorem in these areas motivated the quest for a simpler proof. We use the notation and definitions of [4], without recalling them, but we note the following. The intuitive meaning of the kind of semantics for programs introduced in [4] (called relational runs) has been elaborated and explained in [8, 9] in detail. Also, the connections with various famous program verification methods (in their original forms) like Floyd's, Burstall-Manna-Waldinger's, and Pnueli's are expounded there. Throughout, we work in usual classical first order logic (L), where ~ denotes semantical consequence and ~denotes provability (by any complete inference system for first-order logic). By the completeness theorem of first-order logic, we have that T ~ ~p holds if and only if T ~q~, for any theory T ~_ L and formula tp ~ L.