Dixon结式生成非线性循环不变式算法

"用Dixon结式产生非线性循环不变式 (2012年) - 四川大学学报(工程科学版)，作者：余伟，冯勇" 本文主要探讨了如何在软件验证领域中解决循环程序的部分正确性问题，提出了一种基于Dixon结式生成非线性循环不变式的算法。循环不变式是证明程序正确性的重要工具，它是在循环的每次迭代中都保持不变的性质，能够帮助分析循环的行为并确保其正确运行。 首先，作者将循环程序转化为代数变迁系统（Algebraic Transition System），这是一种形式化的方法，用于描述程序的状态变化和状态之间的关系。这种转化使得程序的动态行为可以用代数关系来表示，便于后续的数学分析。 接下来，算法的关键步骤是结合代数变迁关系和不变式模板构造一个多项式组。不变式模板是一组预先定义的表达式，它们可以用来表达潜在的不变性质。通过这些模板，可以生成一组多项式，这些多项式反映了程序在循环中的行为约束。 然后，算法利用Dixon结式（Dixon Resultant）来处理这个多项式组。Dixon结式是一种在多项式环中寻找共同根的工具，它可以有效地计算出多项式方程组的解集。在本算法中，计算Dixon结式可以得到与模板变量相关的约束系统，这些约束描述了可能的不变式必须满足的条件。 最后，通过对这个约束系统的求解，可以找到满足条件的模板变量的值，从而得到具体的循环不变式。这种方法适用于单路径和多路径的循环程序，表明其具有广泛的适用性。 文章指出，实例分析证明了该算法的有效性，无论是在简单的单路径循环还是复杂的多路径循环中，都能成功地生成非线性的循环不变式，从而有助于程序的正确性验证。 关键词：循环不变式、Dixon结式、模板、约束 这篇论文属于工程技术领域，对于软件验证和形式化方法的研究者具有较高的参考价值，它提供了一种新的、利用代数和约束解决程序正确性问题的方法。