Extending Hoare Logic with an Infinite While-Rule

In the 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‘2 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 relative completeness which is also a first order property.

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 relative completeness which is also a first-order property.