论文部分内容阅读
In this paper we generalize the while-rule in Hoare calculus to an infinite one and then presenta sufficient condition much weaker than the expressiveness for Cook’s relative completeness theoremwith respect to our new axiomatic system. Using the extended Hoare calculus we can derive trueHoare formulas which contain while- statements free of loop invariants. It is also pointed out thatthe weak condition is a first order property and therefore provides a possible approach to thecharacterization 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 presenta sufficient condition much weaker than the expressiveness for Cook’s relative completeness theoremwith respect to our new axiomatic system. Using the extended Hoare calculus we can derive trueHoare 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.