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

《基于消元法生成非线性循环不变式》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、基于消元法生成非线性循环不变式摘要本文基于消元法生成非线性循环不变式的相关算法。程序首先被转换成代数变迁系统，再根据其代数变迁关系和不变式模板构造一个多项式组，把不变式模板中适当变量通过消元法消去，则可以得到关于模板变量的约束关系，通过对该约束关系求解就得到循环不变式。经实例分析，该算法可广泛应用于线性、非线性循环不变式的生成。【关键词】循环不变式消元法模板约束1引言为了证明程序的部分正确性，Floyd、Dijkstra和Gries等引入了循环不变式。生成循环不变式的方法有多种，抽象解释技术是应用得最多的一种

2、方法，但其不足之处是会产生弱的循环不变式。近年来，基于消元法的方法被大量的用于程序验证，包括自动生成循环不变式和对循环程序进行终止性判定，例如基于Grobner基的方法基于Dixon结式和吴方法。基于消元法的循环不变式生成方法首先将循环程序转换成一个代数变迁系统，再由此代数变迁系统得到一个约束求解问题，通过对此约束求解问题求解，最终得到循环程序的循环不变式。10本文首先介绍了代数变迁系统的基本理论、结合消元法和约束求解系统，然后对循环不变式的产生进行了总结和分析。2基础知识2.1定义1代数变迁系统一个代数变迁

3、系统是一个系统，其中：（1）V是一个集合，由有限个变量构成，每个变量对应于循环程序中的变量；（2）L是循环程序的位置集合，这个集合也是有限的；（3）是程序循环的初始位置；（4）Θ是变量集合V上的初始代数断言；（5）T表示状态变迁集。状态变迁τ是它的元素。状态变迁τ是一个三元组，其中l，l′∈L都表示程序位置，分别位于状态变迁之前和之后。当前状态变量集合用V表示，变迁后的状态变量集合用V’表示。ρτ是一个变迁关系，它是上的一个代数断言。对于一个代数变迁系统，如果V’中的变量可以全部用V中变量表示成多项式，则我们

4、称该变迁关系是可分离的，那么我们可以沿着程序的任意路径组合变迁关系。2.2定义2归纳断言一个断言η如果同时满足下面的两个条件，则它是归纳的：初始约束条件：在程序的初始位置10，断言η成立，即由初始代数断言可以得出结论连续性约束条件：对于每一个状态变迁都能根据状态变迁之前的断言和变迁关系得到变迁之后的断言，即。由循环不变式的特点易知，如果某个代数断言是一个循环程序转变的代数变迁系统的不变式，则要求这个代数断言满足归纳断言的两个条件。我们研究的循环不变式是能揭示程序某些特性的多项式。这些多项式都是由程序变量构成的

5、，这些多项式每项的系数是可以变化的。因此，多项式的集合可以用一个模板来表示，其系数由模板变量组成的线性表达式来表示。当我们把模板中模板变量值确定以后，该多项式也就确定了，这样就得到了关于该程序的循环不变式。3循环不变式的生成给定一个代数变迁系统，我们首先把代数变迁系统中的初始位置和位置集合中的其他位置都映射到一个预先给定的模板。然后我们根据变迁系统的变迁关系依次得到每个位置上关于模板变量的约束关系，以保证这些约束的解对应于一个归纳断言映射。10当模板变量实例化时，则不变式模板被特例化到一个多项式断言映射。这个

6、约束求解分为两个部分，分别是对归纳断言的初始化条件和连续性条件进行求解。实际上，如果变迁系统是可以分离的，则可以根据程序选择一组恰当的切点来完成对模板变量约束关系的构造，这是很容易完成的。一个归纳的模板映射的所有约束关系是由其初始约束条件和连续性约束条件联合构成的。令为初始约束，为对应于变迁关系的连续性约束。那么，所有约束如下：。3.1初始约束条件在代数变迁系统的初始位置，初始断言恒为真，由初始位置得到的断言映射也为真，因此初始断言的多项式与的多项式有公共零点。把初始断言的多项式与的多项式组成一个多项式组PS

7、1，通过消元法把多项式组PS1中的一些程序变量消去，就得到该多项式组具有公共零点的约束条件，从而得到初始约束条件。算法如下：（1）构造关于程序变量的多项式组PS1，该多项式组由不变式模板和初始位置断言映射的多项式组成；（2）通过消元法把循环不变式模板中的程序变量消去，如果得到的结果为0，则说明该模板形式的循环不变式在此循环中不存在，需要构造其他形式的模板，如具有更高阶的模板，再从（1）开始；如果得到的结果不为0，则进行第（3）步；（3）令消除了程序变量的多项式中每一项的系数表达式都为0，则得到关于模板变量的约

8、束关系。这些约束关系的联合就构成了初始约束条件。103.2连续性约束条件连续性约束条件的得出与初始约束条件的产生是类似的。如前所述，一个代数变迁系统的连续性具有形式。中的变量值由变迁关系p和状态变迁前位置li中的变量得来，因此，把中的多项式与变迁关系p中的多项式组成一个多项式组PS2，则多项式组PS2有公共零点。那么，通过消元法计算多项式组PS2消除程序变量，结合即可以得到循环不变式模板中每项系数表