Prospects and Limitations of Automatic Assertion Generation for Loop Programs
Jayadev Misra · SIAM Journal on Computing · 1977
The problem of generation of loop invariants from the input, output assertions of a loop program $({\textbf{while }}B{\textbf{ do }}S)$ is considered. The problem is theoretically unsolvable in general. As a special case we consider assertions of the form $xRy$, where R denotes a binary relation, x denotes the variables manipulated by the program and y denotes variables that are not modified by the(program. We derive conditions for R such that if any loop program has $xRy$ as the input and output assertions, then $xRy$ is a loop invariant. These conditions for R are shown to be necessary and sufficient in that if some $R'$ does not meet these conditions, then there are loop programs for which $xR'y$ holds at entrance and exit, though not following every iteration. In particular it is shown that if R is an equivalence relation, then under certain reasonable restrictions on the loop, $xRy$ holds at entrance and exit of the loop if and only if it holds after every iteration.