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

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

Non-linear Loop Invariant Generation Using Dxion Resultant

To solve the partial correct problem of loop program, this paper presented an algorithm 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 algebraic transition system, then a polynomial set was constructed from algebraic transition relation and invariant template, and a constraint system w.r.t template variable was obtained by computing Dixon resultant, finally the constraint system was resolved to get invariant. The algorithm was effective when applied to whether single-path or multi-path programs through case study.