Spain, July 2004.

Enric Rodriguez-Carbonell and Deepak Kapur

In a recent paper by Rodriguez-Carbonell and Kapur, 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 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.