In [rodrikapurIJCAR03], an abstract
framework for automatically generating
loop invariants of imperative programs was proposed. This
framework was then instantiated for the language of conjunctions of polynomial
equations for expressing
loop invariants. This paper presents an algebraic foundation of the
approach. It is first shown that the set of polynomials serving as loop
invariants has the algebraic
structure of an ideal. Using this connection,
it is proved that the procedure for finding invariants can be expressed using
operations
on ideals, for which Groebner
basis constructions can be employed.
Most importantly, it is proved that if the assignment
statements in a loop are solvable in particular, affine mappings with
positive eigenvalues, then the procedure terminates in at most 2m+1
iterations, where m is the number of variables changing in the loop. The proof
is done by showing
that the irreducible subvarieties of the variety associated with a polynomial
ideal approximating the invariant polynomial ideal of the loop
either stay the same or increase their dimension in every iteration.
This yields a correct and complete
algorithm for inferring conjunctions of polynomial equations as invariants.
The method has been implemented in
Maple using the Groebner package. The implementation has been used to
automatically
discover nontrivial invariants for several examples to illustrate the power of
the technique.
