Verifying safety conditions and establishing partial correctness of programs is
one use case of invariant generation. Consider for example the
program in Figure REF , annotated with pre- and
post-conditions specified respectively by the requires and ensures
constructs.
The program of Figure REF  is clearly safe
as the post-condition is satisfied when the loop is exited.
However, to prove program safety
we need additional
loop properties, i.e. inductive loop invariants,
that hold at any loop iteration. It is not hard to derive that after any
iteration \(n\)  of the loop (assuming \(0\le n \le N\) ), the linear
invariant relation \(y\le N\)  holds. It is also not
hard to argue that, upon exiting the loop, the value of \(y\)  is \(N\) .
However, such properties do not give us much
information about the (integer-valued) program variable \(x\) .
For proving program safety, we need to derive loop invariants relating
the values of \(x, y, z\)  at an arbitrary loop iteration \(n\) .
Our work in [1]} generates
such loop invariants by computing the polynomial ideal
\({I=\langle x-y^2, z-2y \rangle }\)  as the so-called polynomial
invariant ideal. The conjunction \(x=y^2\ \wedge z=2y\)  of the polynomial relations corresponding to the basis polynomials of \(I\)  is an
inductive loop invariant, which together with the invariant \(y\le N\) 
is sufficient to prove partial correctness of
Figure REF .
