摘 要

本文基于消元法生成非線性循環(huán)不變式的相關(guān)算法。程序首先被轉(zhuǎn)換成代數(shù)變遷系統(tǒng)， 再根據(jù)其代數(shù)變遷關(guān)系和不變式模板構(gòu)造一個多項式組， 把不變式模板中適當變量通過消元法消去，則可以得到關(guān)于模板變量的約束關(guān)系， 通過對該約束關(guān)系求解就得到循環(huán)不變式。 經(jīng)實例分析， 該算法可廣泛應(yīng)用于線性、非線性循環(huán)不變式的生成。

【關(guān)鍵詞】循環(huán)不變式 消元法 模板 約束

1 引言

為了證明程序的部分正確性，F(xiàn)loyd、Dijkstra和Gries等引入了循環(huán)不變式。生成循環(huán)不變式的方法有多種，抽象解釋技術(shù)是應(yīng)用得最多的一種方法，但其不足之處是會產(chǎn)生弱的循環(huán)不變式。

近年來，基于消元法的方法被大量的用于程序驗證，包括自動生成循環(huán)不變式和對循環(huán)程序進行終止性判定，例如基于Grobner基的方法基于Dixon結(jié)式和吳方法。 基于消元法的循環(huán)不變式生成方法首先將循環(huán)程序轉(zhuǎn)換成一個代數(shù)變遷系統(tǒng)，再由此代數(shù)變遷系統(tǒng)得到一個約束求解問題，通過對此約束求解問題求解，最終得到循環(huán)程序的循環(huán)不變式。

本文首先介紹了代數(shù)變遷系統(tǒng)的基本理論、結(jié)合消元法和約束求解系統(tǒng)，然后對循環(huán)不變式的產(chǎn)生進行了總結(jié)和分析。

2 基礎(chǔ)知識

2.1 定義1 代數(shù)變遷系統(tǒng)

一個代數(shù)變遷系統(tǒng)是一個系統(tǒng)，其中：

（1）V是一個集合，由有限個變量構(gòu)成，每個變量對應(yīng)于循環(huán)程序中的變量；

（2）L是循環(huán)程序的位置集合，這個集合也是有限的；

（3）是程序循環(huán)的初始位置；

（4）Θ是變量集合V 上的初始代數(shù)斷言；

（5）T表示狀態(tài)變遷集。狀態(tài)變遷τ是它的元素。狀態(tài)變遷τ是一個三元組，其中l(wèi)， l′∈L都表示程序位置，分別位于狀態(tài)變遷之前和之后。當前狀態(tài)變量集合用V表示， 變遷后的狀態(tài)變量集合用V'表示。ρτ 是一個變遷關(guān)系， 它是 上的一個代數(shù)斷言。

對于一個代數(shù)變遷系統(tǒng)，如果V中的變量可以全部用V中變量表示成多項式，則我們稱該變遷關(guān)系是可分離的，那么我們可以沿著程序的任意路徑組合變遷關(guān)系。

2.2 定義2 歸納斷言

一個斷言η如果同時滿足下面的兩個條件，則它是歸納的：初始約束條件：在程序的初始位置 ，斷言η成立，即由初始代數(shù)斷言可以得出結(jié)論

連續(xù)性約束條件： 對于每一個狀態(tài)變遷 都能根據(jù)狀態(tài)變遷之前的斷言和變遷關(guān)系得到變遷之后的斷言，即。

由循環(huán)不變式的特點易知， 如果某個代數(shù)斷言是一個循環(huán)程序轉(zhuǎn)變的代數(shù)變遷系統(tǒng)的不變式，則要求這個代數(shù)斷言滿足歸納斷言的兩個條件。

我們研究的循環(huán)不變式是能揭示程序某些特性的多項式。這些多項式都是由程序變量構(gòu)成的，這些多項式每項的系數(shù)是可以變化的。因此，多項式的集合可以用一個模板來表示，其系數(shù)由模板變量組成的線性表達式來表示。當我們把模板中模板變量值確定以后，該多項式也就確定了，這樣就得到了關(guān)于該程序的循環(huán)不變式。

3 循環(huán)不變式的生成

給定一個代數(shù)變遷系統(tǒng)，我們首先把代數(shù)變遷系統(tǒng)中的初始位置和位置集合中的其他位置都映射到一個預(yù)先給定的模板。 然后我們根據(jù)變遷系統(tǒng)的變遷關(guān)系依次得到每個位置上關(guān)于模板變量的約束關(guān)系， 以保證這些約束的解對應(yīng)于一個歸納斷言映射。

當模板變量實例化時，則不變式模板被特例化到一個多項式斷言映射。這個約束求解分為兩個部分，分別是對歸納斷言的初始化條件和連續(xù)性條件進行求解。實際上，如果變遷系統(tǒng)是可以分離的，則可以根據(jù)程序選擇一組恰當?shù)那悬c來完成對模板變量約束關(guān)系的構(gòu)造，這是很容易完成的。

一個歸納的模板映射的所有約束關(guān)系是由其初始約束條件和連續(xù)性約束條件聯(lián)合構(gòu)成的。令為初始約束，為對應(yīng)于變遷關(guān)系 的連續(xù)性約束。那么，所有約束如下：

。

3.1 初始約束條件

在代數(shù)變遷系統(tǒng)的初始位置，初始斷言 恒為真，由初始位置得到的斷言映射也為真，因此初始斷言的多項式與的多項式有公共零點。把初始斷言的多項式與的多項式組成一個多項式組PS1，通過消元法把多項式組PS1中的一些程序變量消去，就得到該多項式組具有公共零點的約束條件，從而得到初始約束條件。算法如下：

（1）構(gòu)造關(guān)于程序變量的多項式組PS1，該多項式組由不變式模板和初始位置斷言映射的多項式組成；

（2） 通過消元法把循環(huán)不變式模板中的程序變量消去，如果得到的結(jié)果為0，則說明該模板形式的循環(huán)不變式在此循環(huán)中不存在，需要構(gòu)造其他形式的模板，如具有更高階的模板，再從（1）開始；如果得到的結(jié)果不為0，則進行第（3）步；

（3）令消除了程序變量的多項式中每一項的系數(shù)表達式都為0，則得到關(guān)于模板變量的約束關(guān)系。 這些約束關(guān)系的聯(lián)合就構(gòu)成了初始約束條件。

3.2 連續(xù)性約束條件

連續(xù)性約束條件的得出與初始約束條件的產(chǎn)生是類似的。

如前所述，一個代數(shù)變遷系統(tǒng)的連續(xù)性具有形式 。 中的變量值由變遷關(guān)系p和狀態(tài)變遷前位置li中的變量得來，因此， 把 中的多項式與變遷關(guān)系p中的多項式組成一個多項式組PS2，則多項式組PS2有公共零點。那么，通過消元法計算多項式組PS2消除程序變量，結(jié)合 即可以得到循環(huán)不變式模板中每項系數(shù)表達式的約束關(guān)系。具體算法如下：

（1）構(gòu)造關(guān)于程序變量的多項式組PS2，該多項式組由狀態(tài)變遷后的模板和變遷關(guān)系中的多項式組成；

（2）通過消元法把模板中的帶撇程序變量消去，如果得到的結(jié)果為0， 則說明該模板形式的循環(huán)不變式在此循環(huán)中不存在，需要構(gòu)造其他形式的模板，如具有更高階的模板，再從（1）開始；如果得到的結(jié)果不為0，則進行第（3）步；endprint

（3）將消除了帶撇程序變量的多項式中每一項的系數(shù)表達式與狀態(tài)變遷之前的 多項式中的系數(shù)一一對應(yīng)起來，則得到關(guān)于模 板變量的約束關(guān)系，從而得到程序連續(xù)性的約束條件。

3.3 約束求解

由于，對代數(shù)變遷系統(tǒng)的初始約束條件和連續(xù)性約束條件進去聯(lián)合求解，其結(jié)果就是我們所要尋找的循環(huán)不變式。

4 實例

無論是單分支的循環(huán)程序，還是多分支的循環(huán)程序， 基于消元法產(chǎn)生循環(huán)不變式的算法都是比較有效的，因此，它可以廣泛的被應(yīng)用于各種程序的部分正確性的驗證。下面就以奇數(shù)求和問題為例，說明算法的有效性。

奇數(shù)求和可以表示成，其程序如下：

integer

此程序中，i的作用是記錄循環(huán)運行次數(shù)的變量。根據(jù)上述程序， 我們設(shè)其一次模板為：

。

初始化條件為：

連續(xù)性條件為：

根據(jù)和，故得此程序的一次循環(huán)不變式為，即，通過此循環(huán)不變式則循環(huán)體內(nèi)每次運算的奇數(shù)與循環(huán)次數(shù)的關(guān)系一目了然了。

假設(shè)其二次循環(huán)不變式模板為：

。

其初始化條件則為：。

連續(xù)性條件為：

根據(jù)和，得此程序的二次循環(huán)不變式為 。

根據(jù)前面計算出來的一次循環(huán)不變式，可以把二次循環(huán)不變式中的變量 消去，則得到改變后的循環(huán)不變式，即。從此循環(huán)不變式，可以輕易看出 是循環(huán)次數(shù) 的平方。

5 總結(jié)

本文將循環(huán)程序轉(zhuǎn)換為一個代數(shù)變遷系統(tǒng)， 結(jié)合模板技術(shù)， 首先用構(gòu)造的模板和代數(shù)變遷系統(tǒng)的變遷關(guān)系構(gòu)造出一個多項式組。再通過消元法消除多項式組中的程序變量，得到程序循環(huán)不變式成立必須滿足的初始約束條件和連續(xù)性約束條件。最后，對此代數(shù)變遷系統(tǒng)的初始約束條件和連續(xù)性約束條件聯(lián)合求解，從而得到對應(yīng)的循環(huán)程序的循環(huán)不變式。 這種方法對于單分支和多分支的程序都有效，只要模板選擇得當，對于循環(huán)不變式的次數(shù)也是沒有限制的，可以得到線性的循環(huán)不變式，也可以得到非線性的循環(huán)不變式。

參考文獻

[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結(jié)式產(chǎn)生非線性循環(huán)不變式[J].四川大學(xué)學(xué)報（工程科學(xué)版），44（04）：115-121，2012，07.

[14]周寧，吳盡昭，王超.基于吳方法的不變式生成算法，[J].北京交通大學(xué)學(xué)報，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-），男，四川省通江縣人。博士學(xué)位?，F(xiàn)為成都師范學(xué)院計算機系副教授。研究方向為程序驗證。

作者單位

成都師范學(xué)院計算機系 四川省成都市 611130endprint