Loop invariants are properties of a program loop that hold both before and after each iteration of the loop. They are often used to verify programs and ensure that algorithms consistently produce correct results during execution. Consequently, generating invariants becomes a crucial task for loops. We specifically focus on polynomial loops, where both the loop conditions and the 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 can have arbitrary degrees. Using tools from algebraic geometry, we present two algorithms designed to generate all polynomial invariants within a given vector subspace, for a branching loop with nondeterministic conditional statements. These algorithms combine linear algebraic subroutines with computations on polynomial ideals. They differ depending on whether the initial values of the loop variables are specified or treated as parameters. Additionally, we present a much more efficient algorithm for generating polynomial invariants of a specific form, applicable to all initial values. This algorithm avoids expensive ideal computations.

翻译：循环不变量是程序循环的一种属性，在循环的每次迭代之前和之后均成立。它们常用于验证程序并确保算法在执行过程中始终产生正确结果。因此，为循环生成不变量成为一项关键任务。我们特别关注多项式循环，即循环条件和循环内的赋值均以多项式表示。尽管为一般循环计算多项式不变量是不可判定的，但对于某些特定类别的循环，已开发出高效算法。例如，当while循环内的所有赋值均涉及线性多项式时，该循环便成为可解的。在本研究中，我们探讨更一般的情况，即多项式可以具有任意次数。利用代数几何中的工具，我们提出了两种算法，旨在为具有非确定性条件语句的分支循环，生成给定向量子空间内的所有多项式不变量。这些算法结合了线性代数子程序与多项式理想的计算。它们根据循环变量的初始值是指定还是作为参数处理而有所不同。此外，我们提出了一种更为高效的算法，用于生成特定形式的多项式不变量，该算法适用于所有初始值，并避免了昂贵的理想计算。