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 ...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.展开更多
文摘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.
