基于消元法生成非線性循環(huán)不變式

《基于消元法生成非線性循環(huán)不變式》由會(huì)員上傳分享，免費(fèi)在線閱讀，更多相關(guān)內(nèi)容在學(xué)術(shù)論文-天天文庫(kù)。

1、基于消元法生成非線性循環(huán)不變式摘要本文基于消元法生成非線性循環(huán)不變式的相關(guān)算法。程序首先被轉(zhuǎn)換成代數(shù)變遷系統(tǒng)，再根據(jù)其代數(shù)變遷關(guān)系和不變式模板構(gòu)造一個(gè)多項(xiàng)式組，把不變式模板中適當(dāng)變量通過(guò)消元法消去，則可以得到關(guān)于模板變量的約束關(guān)系，通過(guò)對(duì)該約束關(guān)系求解就得到循環(huán)不變式。經(jīng)實(shí)例分析，該算法可廣泛應(yīng)用于線性、非線性循環(huán)不變式的生成。【關(guān)鍵詞】循環(huán)不變式消元法模板約束1引言為了證明程序的部分正確性，F(xiàn)loyd、Dijkstra和Gries等引入了循環(huán)不變式。生成循環(huán)不變式的方法有多種，抽象解釋技術(shù)是應(yīng)用得最多的一種

2、方法，但其不足之處是會(huì)產(chǎn)生弱的循環(huán)不變式。近年來(lái)，基于消元法的方法被大量的用于程序驗(yàn)證，包括自動(dòng)生成循環(huán)不變式和對(duì)循環(huán)程序進(jìn)行終止性判定，例如基于Grobner基的方法基于Dixon結(jié)式和吳方法?；谙ǖ难h(huán)不變式生成方法首先將循環(huán)程序轉(zhuǎn)換成一個(gè)代數(shù)變遷系統(tǒng)，再由此代數(shù)變遷系統(tǒng)得到一個(gè)約束求解問(wèn)題，通過(guò)對(duì)此約束求解問(wèn)題求解，最終得到循環(huán)程序的循環(huán)不變式。10本文首先介紹了代數(shù)變遷系統(tǒng)的基本理論、結(jié)合消元法和約束求解系統(tǒng)，然后對(duì)循環(huán)不變式的產(chǎn)生進(jìn)行了總結(jié)和分析。2基礎(chǔ)知識(shí)2.1定義1代數(shù)變遷系統(tǒng)一個(gè)代數(shù)變遷

3、系統(tǒng)是一個(gè)系統(tǒng)，其中：（1）V是一個(gè)集合，由有限個(gè)變量構(gòu)成，每個(gè)變量對(duì)應(yīng)于循環(huán)程序中的變量；（2）L是循環(huán)程序的位置集合，這個(gè)集合也是有限的；（3）是程序循環(huán)的初始位置；（4）Θ是變量集合V上的初始代數(shù)斷言；（5）T表示狀態(tài)變遷集。狀態(tài)變遷τ是它的元素。狀態(tài)變遷τ是一個(gè)三元組，其中l(wèi)，l′∈L都表示程序位置，分別位于狀態(tài)變遷之前和之后。當(dāng)前狀態(tài)變量集合用V表示，變遷后的狀態(tài)變量集合用V’表示。ρτ是一個(gè)變遷關(guān)系，它是上的一個(gè)代數(shù)斷言。對(duì)于一個(gè)代數(shù)變遷系統(tǒng)，如果V’中的變量可以全部用V中變量表示成多項(xiàng)式，則我們

4、稱該變遷關(guān)系是可分離的，那么我們可以沿著程序的任意路徑組合變遷關(guān)系。2.2定義2歸納斷言一個(gè)斷言η如果同時(shí)滿足下面的兩個(gè)條件，則它是歸納的：初始約束條件：在程序的初始位置10，斷言η成立，即由初始代數(shù)斷言可以得出結(jié)論連續(xù)性約束條件：對(duì)于每一個(gè)狀態(tài)變遷都能根據(jù)狀態(tài)變遷之前的斷言和變遷關(guān)系得到變遷之后的斷言，即。由循環(huán)不變式的特點(diǎn)易知，如果某個(gè)代數(shù)斷言是一個(gè)循環(huán)程序轉(zhuǎn)變的代數(shù)變遷系統(tǒng)的不變式，則要求這個(gè)代數(shù)斷言滿足歸納斷言的兩個(gè)條件。我們研究的循環(huán)不變式是能揭示程序某些特性的多項(xiàng)式。這些多項(xiàng)式都是由程序變量構(gòu)成的

5、，這些多項(xiàng)式每項(xiàng)的系數(shù)是可以變化的。因此，多項(xiàng)式的集合可以用一個(gè)模板來(lái)表示，其系數(shù)由模板變量組成的線性表達(dá)式來(lái)表示。當(dāng)我們把模板中模板變量值確定以后，該多項(xiàng)式也就確定了，這樣就得到了關(guān)于該程序的循環(huán)不變式。3循環(huán)不變式的生成給定一個(gè)代數(shù)變遷系統(tǒng)，我們首先把代數(shù)變遷系統(tǒng)中的初始位置和位置集合中的其他位置都映射到一個(gè)預(yù)先給定的模板。然后我們根據(jù)變遷系統(tǒng)的變遷關(guān)系依次得到每個(gè)位置上關(guān)于模板變量的約束關(guān)系，以保證這些約束的解對(duì)應(yīng)于一個(gè)歸納斷言映射。10當(dāng)模板變量實(shí)例化時(shí)，則不變式模板被特例化到一個(gè)多項(xiàng)式斷言映射。這個(gè)

6、約束求解分為兩個(gè)部分，分別是對(duì)歸納斷言的初始化條件和連續(xù)性條件進(jìn)行求解。實(shí)際上，如果變遷系統(tǒng)是可以分離的，則可以根據(jù)程序選擇一組恰當(dāng)?shù)那悬c(diǎn)來(lái)完成對(duì)模板變量約束關(guān)系的構(gòu)造，這是很容易完成的。一個(gè)歸納的模板映射的所有約束關(guān)系是由其初始約束條件和連續(xù)性約束條件聯(lián)合構(gòu)成的。令為初始約束，為對(duì)應(yīng)于變遷關(guān)系的連續(xù)性約束。那么，所有約束如下：。3.1初始約束條件在代數(shù)變遷系統(tǒng)的初始位置，初始斷言恒為真，由初始位置得到的斷言映射也為真，因此初始斷言的多項(xiàng)式與的多項(xiàng)式有公共零點(diǎn)。把初始斷言的多項(xiàng)式與的多項(xiàng)式組成一個(gè)多項(xiàng)式組PS

7、1，通過(guò)消元法把多項(xiàng)式組PS1中的一些程序變量消去，就得到該多項(xiàng)式組具有公共零點(diǎn)的約束條件，從而得到初始約束條件。算法如下：（1）構(gòu)造關(guān)于程序變量的多項(xiàng)式組PS1，該多項(xiàng)式組由不變式模板和初始位置斷言映射的多項(xiàng)式組成；（2）通過(guò)消元法把循環(huán)不變式模板中的程序變量消去，如果得到的結(jié)果為0，則說(shuō)明該模板形式的循環(huán)不變式在此循環(huán)中不存在，需要構(gòu)造其他形式的模板，如具有更高階的模板，再?gòu)模?）開(kāi)始；如果得到的結(jié)果不為0，則進(jìn)行第（3）步；（3）令消除了程序變量的多項(xiàng)式中每一項(xiàng)的系數(shù)表達(dá)式都為0，則得到關(guān)于模板變量的約

8、束關(guān)系。這些約束關(guān)系的聯(lián)合就構(gòu)成了初始約束條件。103.2連續(xù)性約束條件連續(xù)性約束條件的得出與初始約束條件的產(chǎn)生是類似的。如前所述，一個(gè)代數(shù)變遷系統(tǒng)的連續(xù)性具有形式。中的變量值由變遷關(guān)系p和狀態(tài)變遷前位置li中的變量得來(lái)，因此，把中的多項(xiàng)式與變遷關(guān)系p中的多項(xiàng)式組成一個(gè)多項(xiàng)式組PS2，則多項(xiàng)式組PS2有公共零點(diǎn)。那么，通過(guò)消元法計(jì)算多項(xiàng)式組PS2消除程序變量，結(jié)合即可以得到循環(huán)不變式模板中每項(xiàng)系數(shù)表