Generating All Polynomial Invariants in Simple Loops

This paper presents a method for automatically generating all polynomial invariants in simple loops. It is rst shown that the set of polynomials serving as loop invariants has the algebraic structure of an ideal. Based on this connection, a xpoint procedure using operations on ideals and Grobner basis constructions is proposed for nding all polynomial invariants. Most impor-tantly, it is proved that the procedure terminates in at most m + 1 iterations, where m is the number of program variables. The proof relies on showing that the irreducible components of the varieties associated with the ideals generated by the procedure either remain the same or increase their dimension at every iteration of the xpoint procedure. This yields a correct and complete algorithm for inferring conjunctions of polynomial equalities as invariants. The method has been implemented in Maple using the Groebner package. The implementation has been used to automatically discover non-trivial invariants for several examples to illustrate the power of the technique