Generating all polynomial invariants in simple loops
Generating all polynomial invariants in simple loops
复制标题
DOI：
10.1016/j.jsc.2007.01.002
复制
发表时间：
2007-04
期刊：
影响因子：
--
通讯作者：
Enric Rodríguez-carbonell;D. Kapur
中科院分区：
文献类型：
--
作者：
Enric Rodríguez-carbonell;D. Kapur
本文提出了一种在简单循环中自动生成所有多项式不变量的方法。首先证明了作为循环不变量的多项式集合具有理想的代数结构。基于这种联系，提出了一种使用理想运算和 Gröbner 基构造的不动点程序来查找所有多项式不变量。最重要的是，证明了该过程最多在 m+1 次迭代中终止，其中 m 是程序变量的数量。证明依赖于表明与该过程生成的理想相关的簇的不可约分量在固定点过程的每次迭代中要么保持不变，要么增加其维度。这产生了一个正确且完整的算法，用于将多项式等式的合取推断为不变量。该方法已使用 Groebner 包在 Maple 中实现。该实现已用于自动发现一些示例的重要不变量，以说明该技术的强大功能。
This paper presents a method for automatically generating all polynomial invariants in simple loops. It is first shown that the set of polynomials serving as loop invariants has the algebraic structure of an ideal. Based on this connection, a fixpoint procedure using operations on ideals and Gröbner basis constructions is proposed for finding all polynomial invariants. Most importantly, 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 fixpoint 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.