非线性循环不变式的自动生成

摘要

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