Recursive assertions are not enough - or are they?

AbstractCall a set of assertions A complete (with respect to a class of programs S) if for any p, q∈A and S∈S, wherever {p}S{q} holds, then all intermediate assertions can be chosen from A. This paper is devoted to the study of the problem which sets of assertions are complete in the above sense. We prove that any set of recursive assertions containing true and false is not complete. We prove the completeness for while programs of some more powerful assertions, e.g. the set of recursively enumerable assertions. Finally, we show that by allowing the use of an ‘auxilliary’ coordinate, the set of recursive assertions is complete for while programs