基于消元法生成非线性循环不变式

摘 要

本文基于消元法生成非线性循环不变式的相关算法。程序首先被转换成代数变迁系统， 再根据其代数变迁关系和不变式模板构造一个多项式组， 把不变式模板中适当变量通过消元法消去，则可以得到关于模板变量的约束关系， 通过对该约束关系求解就得到循环不变式。 经实例分析， 该算法可广泛应用于线性、非线性循环不变式的生成。

【关键词】循环不变式 消元法 模板 约束

1 引言

为了证明程序的部分正确性，Floyd、Dijkstra和Gries等引入了循环不变式。生成循环不变式的方法有多种，抽象解释技术是应用得最多的一种方法，但其不足之处是会产生弱的循环不变式。

近年来，基于消元法的方法被大量的用于程序验证，包括自动生成循环不变式和对循环程序进行终止性判定，例如基于Grobner基的方法基于Dixon结式和吴方法。 基于消元法的循环不变式生成方法首先将循环程序转换成一个代数变迁系统，再由此代数变迁系统得到一个约束求解问题，通过对此约束求解问题求解，最终得到循环程序的循环不变式。

本文首先介绍了代数变迁系统的基本理论、结合消元法和约束求解系统，然后对循环不变式的产生进行了总结和分析。

2 基础知识

2.1 定义1 代数变迁系统

一个代数变迁系统是一个系统，其中：

（1）V是一个集合，由有限个变量构成，每个变量对应于循环程序中的变量；

（2）L是循环程序的位置集合，这个集合也是有限的；

（3）是程序循环的初始位置；

（4）Θ是变量集合V 上的初始代数断言；

（5）T表示状态变迁集。状态变迁τ是它的元素。状态变迁τ是一个三元组，其中l， l′∈L都表示程序位置，分别位于状态变迁之前和之后。当前状态变量集合用V表示， 变迁后的状态变量集合用V'表示。ρτ 是一个变迁关系， 它是 上的一个代数断言。

对于一个代数变迁系统，如果V中的变量可以全部用V中变量表示成多项式，则我们称该变迁关系是可分离的，那么我们可以沿着程序的任意路径组合变迁关系。

2.2 定义2 归纳断言

一个断言η如果同时满足下面的两个条件，则它是归纳的：初始约束条件：在程序的初始位置 ，断言η成立，即由初始代数断言可以得出结论

连续性约束条件： 对于每一个状态变迁 都能根据状态变迁之前的断言和变迁关系得到变迁之后的断言，即。

由循环不变式的特点易知， 如果某个代数断言是一个循环程序转变的代数变迁系统的不变式，则要求这个代数断言满足归纳断言的两个条件。

我们研究的循环不变式是能揭示程序某些特性的多项式。这些多项式都是由程序变量构成的，这些多项式每项的系数是可以变化的。因此，多项式的集合可以用一个模板来表示，其系数由模板变量组成的线性表达式来表示。当我们把模板中模板变量值确定以后，该多项式也就确定了，这样就得到了关于该程序的循环不变式。

3 循环不变式的生成

给定一个代数变迁系统，我们首先把代数变迁系统中的初始位置和位置集合中的其他位置都映射到一个预先给定的模板。 然后我们根据变迁系统的变迁关系依次得到每个位置上关于模板变量的约束关系， 以保证这些约束的解对应于一个归纳断言映射。

当模板变量实例化时，则不变式模板被特例化到一个多项式断言映射。这个约束求解分为两个部分，分别是对归纳断言的初始化条件和连续性条件进行求解。实际上，如果变迁系统是可以分离的，则可以根据程序选择一组恰当的切点来完成对模板变量约束关系的构造，这是很容易完成的。

一个归纳的模板映射的所有约束关系是由其初始约束条件和连续性约束条件联合构成的。令为初始约束，为对应于变迁关系 的连续性约束。那么，所有约束如下：

。

3.1 初始约束条件

在代数变迁系统的初始位置，初始断言 恒为真，由初始位置得到的断言映射也为真，因此初始断言的多项式与的多项式有公共零点。把初始断言的多项式与的多项式组成一个多项式组PS1，通过消元法把多项式组PS1中的一些程序变量消去，就得到该多项式组具有公共零点的约束条件，从而得到初始约束条件。算法如下：

（1）构造关于程序变量的多项式组PS1，该多项式组由不变式模板和初始位置断言映射的多项式组成；

（2） 通过消元法把循环不变式模板中的程序变量消去，如果得到的结果为0，则说明该模板形式的循环不变式在此循环中不存在，需要构造其他形式的模板，如具有更高阶的模板，再从（1）开始；如果得到的结果不为0，则进行第（3）步；

（3）令消除了程序变量的多项式中每一项的系数表达式都为0，则得到关于模板变量的约束关系。 这些约束关系的联合就构成了初始约束条件。

3.2 连续性约束条件

连续性约束条件的得出与初始约束条件的产生是类似的。

如前所述，一个代数变迁系统的连续性具有形式 。 中的变量值由变迁关系p和状态变迁前位置li中的变量得来，因此， 把 中的多项式与变迁关系p中的多项式组成一个多项式组PS2，则多项式组PS2有公共零点。那么，通过消元法计算多项式组PS2消除程序变量，结合 即可以得到循环不变式模板中每项系数表达式的约束关系。具体算法如下：

（1）构造关于程序变量的多项式组PS2，该多项式组由状态变迁后的模板和变迁关系中的多项式组成；

（2）通过消元法把模板中的带撇程序变量消去，如果得到的结果为0， 则说明该模板形式的循环不变式在此循环中不存在，需要构造其他形式的模板，如具有更高阶的模板，再从（1）开始；如果得到的结果不为0，则进行第（3）步；endprint

（3）将消除了带撇程序变量的多项式中每一项的系数表达式与状态变迁之前的 多项式中的系数一一对应起来，则得到关于模 板变量的约束关系，从而得到程序连续性的约束条件。

3.3 约束求解

由于，对代数变迁系统的初始约束条件和连续性约束条件进去联合求解，其结果就是我们所要寻找的循环不变式。

4 实例

无论是单分支的循环程序，还是多分支的循环程序， 基于消元法产生循环不变式的算法都是比较有效的，因此，它可以广泛的被应用于各种程序的部分正确性的验证。下面就以奇数求和问题为例，说明算法的有效性。

奇数求和可以表示成，其程序如下：

integer

此程序中，i的作用是记录循环运行次数的变量。根据上述程序， 我们设其一次模板为：

。

初始化条件为：

连续性条件为：

根据和，故得此程序的一次循环不变式为，即，通过此循环不变式则循环体内每次运算的奇数与循环次数的关系一目了然了。

假设其二次循环不变式模板为：

。

其初始化条件则为：。

连续性条件为：

根据和，得此程序的二次循环不变式为 。

根据前面计算出来的一次循环不变式，可以把二次循环不变式中的变量 消去，则得到改变后的循环不变式，即。从此循环不变式，可以轻易看出 是循环次数 的平方。

5 总结

本文将循环程序转换为一个代数变迁系统， 结合模板技术， 首先用构造的模板和代数变迁系统的变迁关系构造出一个多项式组。再通过消元法消除多项式组中的程序变量，得到程序循环不变式成立必须满足的初始约束条件和连续性约束条件。最后，对此代数变迁系统的初始约束条件和连续性约束条件联合求解，从而得到对应的循环程序的循环不变式。 这种方法对于单分支和多分支的程序都有效，只要模板选择得当，对于循环不变式的次数也是没有限制的，可以得到线性的循环不变式，也可以得到非线性的循环不变式。

参考文献

[1]Floyd RW.Assigning meanings to programs[C]// Proceedings of Symposia in Applied Mathematics. 1967：19-37.

[2]Dijkstra，E.W.A Discipline of Programming [M].New Jersey：Prentice Hall Inc.，1976.

[3]Gries，D.The Science of Pro-gramming[M].New York：Springer-Verlag1981.

[4]Hoare，C.A.R.An Axiomatic Basis for Computer Programming[J]. Communications of ACM，1969，12（10）： 76-580.

[5]CoustP，Coust R.Abstract interpretation：A unified lattice model for static analysis of programs by construction or approximation of fixpoints[C]//ACM Principles of Programming Languages. New York：ACM Press，1977：238-252.

[6]CousotP，HalbwachsN.Automatic discovery of linear restraints among the variables of a program[C]//ACM Principles of Programming Languages.New York：ACM Press，1978：84-97.

[7]Rodriguez-carbonell E，Kapur D.Gene-rating all polynomial invariants in simple loops[J].Journal of Symbolic Computation，2007，42（4）：443-476.

[8]Muller-olm M，Seidl H.Computing polynomial program invariants[J]. nformation Processing Letters，2004，91 （5）：233-244.

[9]Muller-olm M，Seidl H.Precise interprocedural analysis through linear algebra[C]//ACM SIGPLAN Principles of Programming Languages. New York：ACM Press，2004：330-341.

[10]Sankaranarayanan S，Sipma H B，Manna Z. Non-linear loop invariant generation using Grobner bases[C]//ACM SIGPLAN Principles of Programming Languages.New York：ACM Press，2004：318-329.

[11]Colon M，Sankaranarayanan S，Sipma H. Linear invariant generation using non-linear constraint solving [C]//CAV 2003：Computer2Aided Verification， LNCS 2725.Heidelberg：Springer Verleg，2003：420-433.

[12]Yang L，Zhou C，Zhan N.，Xia R.Recent advances in program verification through computer algebra.Frontiers of Computer Science in China，2010，4（1）：1-16.

[13]余伟，冯勇.用Dixon结式产生非线性循环不变式[J].四川大学学报（工程科学版），44（04）：115-121，2012，07.

[14]周宁，吴尽昭，王超.基于吴方法的不变式生成算法，[J].北京交通大学学报，36（02）：1-7，2012，04.

[15]Yong Cao，Qingxin Zhu.Finding Loop Invariants Based on Wu's Characteristic Set Method. Information Technology Journal. 2010，9（2）：349-353.

作者简介

余伟（1973-），男，四川省通江县人。博士学位。现为成都师范学院计算机系副教授。研究方向为程序验证。

作者单位

成都师范学院计算机系 四川省成都市 611130endprint