基于消元法生成非線性循環不變式

摘 要

本文基于消元法生成非線性循環不變式的相關算法。程序首先被轉換成代數變遷系統， 再根據其代數變遷關系和不變式模板構造一個多項式組， 把不變式模板中適當變量通過消元法消去，則可以得到關于模板變量的約束關系， 通過對該約束關系求解就得到循環不變式。 經實例分析， 該算法可廣泛應用于線性、非線性循環不變式的生成。

【關鍵詞】循環不變式 消元法 模板 約束

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