Inadequacy of Computable Loop Invariants

Hoare logic is a widely recommended verification tool. There is, however, a problem of finding easily-checkable loop invariants; it is known that decidable assertions do not suffice to verify WHILE programs, even when the pre- and post-conditions are decidable. We show here a stronger result: decidable invariants do not suffice to verify single-loop programs. We also show that this problem arises even in extremely simple contexts. Let N be the structure consisting of the set of natural numbers together with the functions S(x)=x+1, D(x)=2x and function H(x) that is equal x/2 rounded down. There is a single-loop program P using only three variables x,y,z such that the asserted program

 x = y = z = 0 {P} false

is partially correct on N but any loop invariant I(x,y,z) for this asserted program is undecidable.