Logic of Hoare

Paper of R.W. Floyd brought some light on proving programs correct. Later C.A.R. Hoare proposed another formalization based on the ideas of Floyd. S. Cook addressed the problem of completeness of Floyd-Hoare calculus and formulated the so called relative completeness theorem.

In the light of the paper [Goraj, Mirkowska, Paluszkiewicz ↓] this theorem is unnecessary. Theorem 5 of this paper states that notions of feasible and of acceptable description of program coincide. In other words if a verification condition of a program is valid in all models of a theory then it is provable from the axioms of the theory. For the details see [AL4software ↓] sections on Floyd's descriptions of programs and Hoare's logic of partial correctness.