Loop invariants are properties of a program loop that hold before and after each iteration of the loop. They are often employed to verify programs and ensure that algorithms consistently produce correct results during execution. Consequently, the generation of invariants becomes a crucial task for loops. We specifically focus on polynomial loops, where both the loop conditions and assignments within the loop are expressed as polynomials. Although computing polynomial invariants for general loops is undecidable, efficient algorithms have been developed for certain classes of loops. For instance, when all assignments within a while loop involve linear polynomials, the loop becomes solvable. In this work, we study the more general case where the polynomials exhibit arbitrary degrees. Applying tools from algebraic geometry, we present two algorithms designed to generate all polynomial invariants for a while loop, up to a specified degree. These algorithms differ based on whether the initial values of the loop variables are given or treated as parameters. Furthermore, we introduce various methods to address cases where the algebraic problem exceeds the computational capabilities of our methods. In such instances, we identify alternative approaches to generate specific polynomial invariants.

翻译：循环不变量是程序循环中在每次迭代前后均成立的性质，常用于程序验证，确保算法在执行过程中持续产生正确结果。因此，不变量生成成为循环验证的关键任务。本文重点关注多项式循环，其中循环条件与循环内的赋值均以多项式形式表示。尽管一般循环的多项式不变量计算不可判定，但针对特定循环类已发展出高效算法。例如，当while循环内所有赋值涉及线性多项式时，该循环具有可解性。本研究进一步探讨多项式具有任意度数的广义情形。运用代数几何工具，我们提出两种算法，用于生成给定度数以下while循环的所有多项式不变量。这两种算法的区别在于循环变量的初始值是已知还是作为参数处理。此外，我们针对代数问题超出计算方法计算能力的情形，引入多种处理策略。在此类情况下，我们提出生成特定多项式不变量的替代方案。