【摘要】 提出了一个自动生成非线性循环不变式的算法。循环不变式可以表示成一个带参数的多项式的形式,根据断言的归纳特性,将循环不变式的生成问题转变成一个约束求解问题,这个约束求解问题的每个解对应于一个循环不变式,如果约束求解问题仅有零解,则说明不存在该参数多项式形式的循环不变式。该算法在Maple中得到了实现,并通过一些实例说明了该算法的有效性。更多还原

【Abstract】 This paper proposed an approach to automatically generate non-linear loop invariants.An invariant of a loop was hypothesized as a parameterized polynomial.Based on the inductive assertion’s properties,we reduced the non-linear loop invariant problem to a numerical constraint solving problem.All the solutions to these constraints were the non-linear loop invariants of the program.The approach has been implemented in Maple.The implementation has been used to automatically discover nontrivial invariants for many programs.更多还原