用Dixon结式产生非线性循环不变式

Non-linear Loop Invariant Generation Using Dxion Resultant

针对循环程序的部分正确性问题,在代数变迁系统理论基础上,结合约束理论提出了一种用Dixon结式生成循环不变式的算法。首先,程序被转换成代数变迁系统,再根据代数变迁关系和不变式模板构造一个多项式组,计算此多项式组的Dixon结式可以得到关于模板变量的约束,最后对该约束系统求解就得到该模板形式的程序不变式。经实例分析,该算法应用于单路径和多路径程序均是有效的。

TO solve the partial correct problem of loop program, an algorithm was presented to generate non-linear loop invariant by computing Dixon resultant based on algebraic transition system and constraint system. The loop program was firstly transformed to an al- gebraic transition system, then a polynomial set was constructed from algebraic transition relation and invariant template, and a con- straint system w. r. t template variable was obtained by computing Dixon resultant. Finally the constraint system was resolved to get in- variant. The algorithm was effective to whether single-path or multi-path programs through case study.