Extending Hoare Logic with an Infinite While-Rule

In this paper we generalize the while-rule in Hoare calculus to an infinite one and then present a sufficient condition much weaker than the expressiveness for Cook s relative completeness theorem with respect to our new axiomatic system. Using the extended Hoare calculus we can derive true Hoare formulas which contain while- statements free of loop invariants. It is also pointed out that the weak condition is a first order property and therefore provides a possible approach to the characterization of relat…