一類單元賦值語句型循環(huán)不變式的開發(fā)方法研究

楊黃磊，薛錦云

(江西師范大學(xué)江西省高性能計(jì)算技術(shù)重點(diǎn)實(shí)驗(yàn)室，江西南昌330022)

0 引言

循環(huán)不變式揭示了循環(huán)程序的本質(zhì)特征，循環(huán)不變式對(duì)于循環(huán)程序的理解、軟件驗(yàn)證、形式化程序設(shè)計(jì)和自動(dòng)程序設(shè)計(jì)至關(guān)重要，甚至部分人認(rèn)為不知道循環(huán)不變式就不可能理解循環(huán)［1］.

循環(huán)不變式的開發(fā)分為手工開發(fā)和自動(dòng)開發(fā).早期采取手工的方式，隨著理論和技術(shù)發(fā)展，自動(dòng)方式被廣泛應(yīng)用于循環(huán)不變式的開發(fā).而自動(dòng)方式又被分為靜態(tài)方法和動(dòng)態(tài)方法.靜態(tài)方法僅分析程序的源代碼本身，其中基于抽象解釋的方法和基于約束的方法是應(yīng)用最廣的系統(tǒng)性方法.抽象解釋是在抽象域上的符號(hào)程序執(zhí)行，其抽象域綜合描述了循環(huán)迭代的語義.P.Cousot和 R.Cousot［2］將抽象解釋更新并擴(kuò)展到處理現(xiàn)代程序語義.基于抽象解釋的不變式生成技術(shù)［3-6］可以構(gòu)造多種類型的線性和多項(xiàng)式循環(huán)不變式.基于約束的技術(shù)依賴于非簡單的數(shù)學(xué)域(例如多項(xiàng)式或者凸面多面體)上的復(fù)雜決策過程來精確地表達(dá)帶有一定模板特性的循環(huán)語義.基于約束技術(shù)同樣可以構(gòu)造出線性和多項(xiàng)式循環(huán)不變式［7］.近10年動(dòng)態(tài)方法開始應(yīng)用于循環(huán)不變式的開發(fā)，其通過選取充足多樣的輸入，然后在執(zhí)行程序的過程中探測(cè)程序的不變式特性.M.D.Ernst等［8］的Daikon技術(shù)表明動(dòng)態(tài)方法在開發(fā)循環(huán)不變式具有實(shí)用性，并且?guī)?dòng)了許多后續(xù)工作［9-13］.B.Meyer等［1］采用的 domain theory，用各個(gè)應(yīng)用領(lǐng)域內(nèi)的具體特征函數(shù)和謂詞高度抽象地表達(dá)包括后置斷言和循環(huán)不變式在內(nèi)的斷言，系統(tǒng)地分析確認(rèn)和分類計(jì)算機(jī)科學(xué)的許多領(lǐng)域的典型算法的循環(huán)不變式，指出循環(huán)不變式呈現(xiàn)與領(lǐng)域相關(guān)的模式特征，以期利用這些模式特征來開發(fā)循環(huán)不變式.

靜態(tài)方法是穩(wěn)健的并且對(duì)于其能開發(fā)出的一類不變式是完備的.利用不變式代表數(shù)學(xué)域的可判定性、可保證穩(wěn)健性和完備性，因而這些技術(shù)處理新的不變式特性時(shí)會(huì)受到不可判定性的制約.動(dòng)態(tài)方法把候選不變式特性中不違背任何一次程序執(zhí)行的不變式特性被當(dāng)做可能的不變式，因此這是不穩(wěn)健的，只是一種啟發(fā)式猜測(cè).動(dòng)態(tài)不變式開發(fā)方法在正確實(shí)現(xiàn)時(shí)能較好地發(fā)揮作用，但對(duì)于許多循環(huán)不變式的開發(fā)仍存在如何獲取充足多樣的測(cè)試集的問題.當(dāng)前動(dòng)態(tài)方法較少應(yīng)用于開發(fā)循環(huán)不變式，但是其主要被應(yīng)用于推導(dǎo)前后置斷言或者中間斷言中.

薛錦云［14］提出的按循環(huán)變量的元數(shù)分類的思路來研究循環(huán)不變式，是一種靜態(tài)方法.單元賦值語句指賦值符號(hào)右邊僅出現(xiàn)1個(gè)與賦值符號(hào)左邊相同的循環(huán)變量且不出現(xiàn)其他的變量(循環(huán)控制變量除外)的賦值語句.從而單元賦值語句型循環(huán)程序就指循環(huán)體里僅出現(xiàn)1條單元賦值語句且不出現(xiàn)其他多元賦值語句的循環(huán)程序.

1 循環(huán)不變式的新定義和新開發(fā)策略

這里的新定義和新的開發(fā)策略［14-15］是由薛錦云提出，定義在循環(huán)程序段中，其值隨著程序的執(zhí)行不斷改變的變量為循環(huán)變量.循環(huán)不變式支配著這些循環(huán)變量的變化，反應(yīng)了它們的變化規(guī)律.因此，薛錦云給出如下定義.

定義1 給定循環(huán)語句DO和它的所有循環(huán)變量的集合A，1個(gè)反應(yīng)A中每1個(gè)循環(huán)變量的變化規(guī)律且在循環(huán)體S執(zhí)行前后均為真的謂詞稱為循環(huán)語句DO的循環(huán)不變式.

本文要研究的單元賦值語句型循環(huán)程序，按定義A集合里僅含1個(gè)循環(huán)變量，就是賦值語句符號(hào)左邊出現(xiàn)的變量.然后需要尋找反應(yīng)該變量的變化規(guī)律，且在循環(huán)體S執(zhí)行前后均為真的謂詞，如此就能得出循環(huán)不變式.

設(shè)問題P的解由解序列由P1，P2，…，Pn構(gòu)成，其中每個(gè)Pi(1≤i≤n)為其右邊某個(gè)Pk子問題的解，Pn為P的解.把Pi和它前面的1個(gè)或者多個(gè)Pj(1≤j≤i)，關(guān)聯(lián)起來的等式叫做問題求解序列的遞推關(guān)系，簡稱為遞推關(guān)系，用Pi=F(Pj)表示，其中Pj為Pi子問題的序列.尋找遞推關(guān)系即把問題P的解表示成它的子問題的解的函數(shù).從而有了開發(fā)循環(huán)不變式的新策略.

策略1 以循環(huán)程序正確性驗(yàn)證條件為基準(zhǔn)，考察循環(huán)初始條件及循環(huán)結(jié)束所得的信息，分析程序所解問題的實(shí)際背景、數(shù)學(xué)性質(zhì)和程序特征，通過歸納推理找出所有循環(huán)變量的變化規(guī)律，即為所求的循環(huán)不變式.

按照以上策略，分析單元賦值語句型問題的實(shí)際背景，數(shù)學(xué)性質(zhì)和程序特征可得遞推關(guān)系由單元賦值語句，結(jié)合初始條件和循環(huán)結(jié)束的信息，由歸納推理可以找到循環(huán)不變式.

2 2種單元賦值語句型循環(huán)不變式開發(fā)方法

按照循環(huán)不變式新的開發(fā)策略，通過對(duì)大量單元賦值語句型循環(huán)程序的研究，發(fā)現(xiàn)單元賦值語句型循環(huán)程序各種各樣，這里通過2個(gè)典型的形式來說明單元賦值語句型循環(huán)程序的開發(fā)規(guī)律.下面分別敘述這2種形式的循環(huán)不變式的開發(fā)步驟及利用Dijkstra最弱前置謂詞［16］方法進(jìn)行正確性證明，為了表述和證明的方便，程序按照Dijkstra衛(wèi)士命令語言書寫.

2.1 第1種循環(huán)程序{Q:in≥i0}

var S:real;var i:integer;

S:=S(0);i:=i0;

do i＜in→S:=p*Sr+q;i:=i+1 od

{R:S=S(in-i0)}

結(jié)合S=S(0)和(?i:i0≤i≤in-1:S(i-i0+1)=p*(S(i-i0))r+q)，當(dāng)i=in-1時(shí)得出后置斷言R:S=S(in-i0))，Q為前置斷言，S為循環(huán)變量，i為循環(huán)控制變量，S(0)、i0、in表示實(shí)數(shù)，單元賦值語句 S:=p*Sr+q中 p、q、r表示實(shí)數(shù)且 p≠0、r≠0.循環(huán)不變式開發(fā)步驟為:

(i)進(jìn)入循環(huán)前，分析循環(huán)初始條件，得到循環(huán)變量S的初始值S(0)及循環(huán)控制變量初始值i0;

(ii)進(jìn)入循環(huán)，首先找到循環(huán)控制條件i＜in.結(jié)合第(i)步，可得循環(huán)不變式合取項(xiàng)S=S(i-i0)∧i0≤i≤in;

(iii)然后找到S:=p*Sr+q，得到問題求解序列的遞推關(guān)系S(i)=p*(S(i-1))r+q;

(iv)將第(ii)步和第(iii)步得到的結(jié)果合取即可得到循環(huán)不變式I:

S=S(i-i0)∧i0≤i≤in∧［S(i)=p*(S(i-1))r+q］.

循環(huán)不變式確認(rèn)及程序正確性證明:

(i)Q?WP("S:=S(0)，i:=i0"，I)，循環(huán)開始前，I成立.

in≥i0?((S=S(i-i0)∧i0≤i≤in∧［S(i)=p*≡{［S(i)=p*(S(i-1))r+q］總為真且不參與文字替換}，in≥i0?S(0)=S(0)∧i0≤i0≤in∧［S(i)=p*(S(i-1))r+q］≡true.

(ii)I∧Guard?WP(″S=p*Sr+q;i=i+1″，I)，Guard表示“i＜in”要保證循環(huán)每次執(zhí)行后不變式成立，進(jìn)行如下證明:

I∧Guard≡S=S(i-i0)∧i0≤i≤in∧［S(i)=p*(S(i-1))r+q］∧i＜ in≡S=S(i-i0)∧i0≤i＜in∧［S(i)=p*(S(i-1))r+q］.

WP(″S=p*Sr+q;i=i+1″，I)≡((S=S(i-i0)∧i0≤i≤in∧［S(i)=p*≡{文字替換}.

p*Sr+q=S(i+1-i0)∧i0≤i+1≤in∧［S(i)=p*(S(i-1))r+q］≡ {利用［S(i)=p*(S(i-1))r+q］對(duì)S(i+1-i0)等量替換}.

p*Sr+q=p*(S(i-i0))r+q∧i0-1≤i＜ in∧［S(i)=p*(S(i-1))r+q］≡S=S(i-i0)∧i0-1≤i＜in∧［S(i)=p*(S(i-1))r+q］.

I∧Guard?WP(″S=p*Sr+q;i=i+1″，I)≡{i0≤i＜in?i0-1≤i＜in}≡true.

(iii)I∧﹁Guard?R循環(huán)不變式和Guard的否定能得到后置斷言成立.

I∧﹁ Guard≡S=S(i-i0)∧i0≤i≤in∧［S(i)=p*(S(i-1))r+q］∧i≥in≡S=S(i-i0)∧i=in∧［S(i)=p*(S(i-1))r+q］≡S=S(in-i0)∧［S(i)=p*(S(i-1))r+q］?S=S(in-i0).

因此，(I∧﹁ Guard?R)≡true.

(iv)循環(huán)的終止性顯然成立.

2.2 第2種循環(huán)程序

{Q:in≥i0}

var S:real;var i:integer;

S:=S(0);i:=in;

do i＞ i0→i:=i-1;S:=p*Sr+a［i］od

{R:S=S(in-i0)}.

結(jié)合S=S(0)和(?i:i0+1≤i≤in:S(in-i+1)=p*(S(in-i))r+a［i-1］)，當(dāng) i=i0+1 時(shí)得出后置斷言R:S=S(in-i0)，開發(fā)步驟如下:

(i)進(jìn)入循環(huán)前，分析循環(huán)初始條件，得到循環(huán)變量S的初值S(0)及循環(huán)控制變量的初值in;

(ii)進(jìn)入循環(huán)，首先得到循環(huán)控制條件i＞i0，結(jié)合第(i)步，可得循環(huán)不變式的合取項(xiàng)

(iii)然后得到 S:=p*Sr+a［i］，可得問題求解序列的遞推關(guān)系S(in-(i-1))=p*(S(ini))r+a［i-1］;

(iv)將第(ii)步和第(iii)步得到的結(jié)果合取即可得循環(huán)不變式I:

S=S(in-i)∧i0≤i≤in∧［S(in-(i-1))=p*(S(in-i))r+a［i-1］］.

循環(huán)不變式確認(rèn)及程序正確性證明:

(i)Q?WP("S:=S(0)，i:=in"，I)，循環(huán)開始前，I成立.

in≥i0?((S=S(in-i)∧i0≤i≤in∧［S(ini+1)=p*{［S(in-i+1)=p*(S(in-i))r+a［i-1］］總為真且不參與文字替換}.in≥i0?S(0)=S(0)∧i0≤in≤in∧［S(in-i+1)=p*(S(in-i))r+a［i-1］］≡true.

(ii)I∧Guard?WP(″i=i-1;S=p*Sr+a［i］″，I)，Guard 表示“i＞ i0”要保證循環(huán)每次執(zhí)行后不變式成立，進(jìn)行以下證明:

I∧Guard≡S=S(in-i)∧i0≤i≤in∧［S(ini+1)=p*(S(in-i))r+a［i-1］］∧i＞ i0≡S=S(in-i)∧i0＜i≤in∧［S(in-i+1)=p*(S(in-i))r+a［i-1］］.WP(″i=i-1;S=p*Sr+a［i］″，I)≡((S=S(ini)∧i0≤i≤in∧［S(in-i+1)=p*(S(in-i))r+≡{文字替換}.p*Sr+a［i-1］=S(in-i+1)∧i0+1≤i≤in+1∧［S(in-i+1)=p*(S(in-i))r+a［i-1］］≡{利用［S(in-i+1)=p*(S(in-i))r+a［i-1］］對(duì)S(in-i+1)等量替換}.

p*Sr+a［i-1］=p*(S(in-i))r+a［i-1］∧i0+1≤i≤in+1∧［S(in-i+1)=p*(S(in-i))r+a［i-1］］≡S=S(in-i)∧i0+1≤i≤in+1∧［S(in-i+1)=p*(S(in-i))r+a［i-1］］.I∧Guard?WP(″i=i-1;S=p*Sr+a［i］″，I)≡{i0＜ i≤in?i0+1≤i≤in+1}≡true.

(iii)I∧﹁Guard?R循環(huán)不變式和Guard的否定能得到后置斷言成立.

I∧﹁ Guard≡S=S(in-i)∧i0≤i≤in∧［S(in-i+1)=p*(S(in-i))r+a［i-1］］∧i≤i0≡S=S(in-i)∧i=i0∧［S(in-i+1)=p*(S(in-i))r+a［i-1］］≡S=S(in-i0)∧［S(in-i+1)=p*(S(in-i))r+a［i-1］］?S=S(in-i0).

因此，I∧﹁ Guard?R≡true.

(iv)循環(huán)的終止性顯然成立.

3 應(yīng)用舉例

本文開發(fā)的循環(huán)不變式具有一定的普遍性，關(guān)鍵就是對(duì)單元賦值語句進(jìn)行了抽象，當(dāng)參數(shù)p、q、r取不同的具體值時(shí)，就可以得到許多該類型的不同循環(huán)程序的循環(huán)不變式.現(xiàn)在列舉3例典型程序說明方法的應(yīng)用.

例1 猴子吃桃問題:有一只猴子第1天摘下若干個(gè)桃子，當(dāng)即吃掉了一半，又多吃了1個(gè);第2天將剩下的桃子吃掉一半，有多吃了1個(gè);按照這樣的吃法，每天都吃前一天剩下的桃子的一半，又多吃1個(gè).到了第10天，就只剩下1個(gè)桃子，編程實(shí)現(xiàn)這只猴子第1天共摘下了多少個(gè)桃子?

{Q:10≥1}

var i:integer;var s:integer;

s:=1;i:=1;

do i＜10→s:=2*s+2;i:=i+1 od

{R:s=s(9)}.

通過觀察，它是第1種情形的具體化，這里p=2，q=2，r=1.

(i)s和i的初值都為1;

(ii)i＜10，循環(huán)不變式的合取項(xiàng)為

(iii)s:=2*s+2，問題求解序列的遞推關(guān)系:s(i)=2*s(i-1)+2;

(iv)將(ii)和(iii)的結(jié)果合取得到循環(huán)不變式:

例2 b進(jìn)制數(shù)轉(zhuǎn)化為十進(jìn)制數(shù).給定任意b進(jìn)制及其指數(shù)位置數(shù)值數(shù)組，將其轉(zhuǎn)化為十進(jìn)制數(shù).例如，5 進(jìn)制及其指數(shù)位置數(shù)值數(shù)組〈3，2，0，1〉，表示十進(jìn)制數(shù)138=3*50+2*51+0*52+1*53.下面的算法程序簡單直接，很容易想到，其本質(zhì)上可以用秦九韶算法求解，它將n-1次多項(xiàng)式的值轉(zhuǎn)化為求n-1個(gè)1次多項(xiàng)式的值，執(zhí)行效率可顯著提高.

{Q:n≥0}

var i:integer;var sum:integer;

var a:array(0:n-1，integer);

sum:=0;i:=0;

do i＜ n→sum:=sum+a［i］*bi;i:=i+1

od

{R:s=s(n)}.

這里單元賦值語句形式類似于第1種情形，開發(fā)步驟相似，其中n、b表示整數(shù):

(i)sum和i的初值都為0;

(ii)i＜n，循環(huán)不變式的合取項(xiàng)為

(iii)sum:=sum+a［i］*bi，問題求解序列的遞推關(guān)系 sum(i)=sum(i-1)+a［i-1］*bi-1;

(iv)將(ii)和(iii)的結(jié)果合取得循環(huán)不變式:

sum=sum(i)∧0≤i≤n∧［sum(i)=sum(i-1)+a［i-1］*bi-1］.

例3 秦九韶算法，求a［n-1］*xn-1+a［n-2］*xn-2+… +a［1］*x+a［0］的值.

{Q:n≥0}

var i:integer;var s:integer;

var a:array(0:n-1，integer);

s:=0;i:=n;

do i＞0→i:=i-1;s:=s*x+a［i］od

{R:s=s(n)}.

通過觀察，它是第2種情形的具體化，這里p=x，r=1，n 為整數(shù).

(i)s和i的初值分別為0和n;

(ii)i＞0，循環(huán)不變式的合取項(xiàng)為s=s(n-i)∧0≤i≤n;

(iii)s=s*x+a［i］，問題求解序列的遞推關(guān)系為 s(n-(i-1))=s(n-i)*x+a［i-1］);

(iv)將(ii)和(iii)的結(jié)果組裝得循環(huán)不變式:

s=s(n-i)∧0≤i≤n∧［s(n-(i-1))=s(n-i)*x+a［i-1］)］.

4 總結(jié)和展望

從上面的介紹可看出，通過抽象概括出單元賦值語句和單元賦值語句型循環(huán)程序的概念，抓住循環(huán)不變式的本質(zhì)特征，在新的開發(fā)策略的指導(dǎo)下，使得一類單元賦值語句型循環(huán)不變式的開發(fā)變得簡單、有效.相比其他的各種開發(fā)方法，可以避免盲目性，確保結(jié)果的可靠性.新的開發(fā)策略提到的分析所解問題的實(shí)際背景、程序特征、數(shù)學(xué)性質(zhì)和Meyer等的domain theory表示斷言(尤其是后置斷言和循環(huán)不變式)，與利用的具體應(yīng)用領(lǐng)域的特征函數(shù)和謂詞思維角度不謀而合.新的開發(fā)策略結(jié)合從循環(huán)不變式的本質(zhì)特征和正確性驗(yàn)證條件得到的不變式穩(wěn)健且有用，而Meyer等的用domain theory表達(dá)的循環(huán)不變式利用程序證明器保證正確理論上并不完全嚴(yán)格正確.

在實(shí)踐上，大量開發(fā)穩(wěn)健而有用的循環(huán)不變式仍是巨大的挑戰(zhàn)，僅單元賦值語句型循環(huán)程序的循環(huán)不變式的構(gòu)造就比較復(fù)雜，本文解決的是部分情形，進(jìn)一步解決需要在數(shù)據(jù)組織結(jié)構(gòu)和不變式的表示理論等方面努力.還可進(jìn)一步擴(kuò)展到多元賦值語句型循環(huán)程序，這有待相關(guān)理論和技術(shù)的進(jìn)步.

［1］ Furia CA，Meyer B，Velder S.Loop invariants:analysis，classification，andexamples［EB/OL］.［2012-10-16］.http://arxiv.org/abs/1211.4470.

［2］Patrick Cousot，Radhia Cousot.Abstract interpretation:a unified latticemodel for static analysis of programs by construction or approximation of fixpoints［C］.New York:ACM press，1997:238-252.

［3］ Mine'A.The octagon abstract domain higher-order and symbolic computation ［J］.High-Order and Symbolic Computation，2006，19(1):31-100.

［4］Patrick Cousot，Nicolas Halbwachs.Automatic discovery of linear restraints among variables of a program［EB/OL］.［2012-10-17］.http:∥www.citeulike.org/user/pganty/article/120467.

［5］ EnricRodr'1guez-Carbonell，Deepak Kapur.Automatic generation of polynomial invariants of bounded degree using abstract interpretation ［J］.Sci Comput Program，2007，64(1):54-75.

［6］EnricRodr'1guez-Carbonell，Deepak Kapur.An abstract interpretation approach for automatic generation of polynomial invariants［J］.SAS，2004，3148:280-295.

［7］ Michael Colón，Sriram Sankaranarayanan，Henny Sipma.Linear invariant generationusing non-linear constraint solving［J］.CAV，2003，2725:420-433.

［8］Michael M D，Cockrell J，Griswold W G，et al.Dynamically discovering likely program invariants to support program evolution ［J］.IEEE Transactions of Software Engineering，2001，27(2):99-123.

［9］Jeff H Perkings，Michael D Ernst.Efficient incremental algorithms for dynamic detection of likely invariants［EB/OL］.［2013-05-16］.http:∥homes.cs.washington.edu/～mernst/pubs/invariants-incremental-fse 2004.pdf.

［10］Christoph Csallner，Nikolai Tillman，Yannis Smaragdakis.DySy:dynamicsymbolic execution for invariant inference［EB/OL］.［2013-07-12］.http:∥research.microsoft.com/apps/pubs/default.aspx?id=70511.

［11］Nadia Polikarpova，Ilinca Ciupa，Bertrand Meyer.A comparative study of programmer-written and automatically inferred contracts［EB/OL］.［2013-07-19］.http:∥se.inf.ethz.ch/people/polikarpova/publications/issta09.pdf.

［12］Yi Wei，F(xiàn)uria CA，Kazmin N，et al.Inferring better contracts［EB/OL］.［2013-08-16］.http:∥doi.ieee computersociety.org/10.1145/1985793.1985820.

［13］Thanhvu Nguyen，Deepak Kapur，Westley Weimer，et al.Using dynamic analysis to discover polynomial and array invariants［EB/OL］.［2013-06-17］.http:∥en.wikipedia.org/wiki/International_conference_on_Software_Engineering.

［14］Xue Jinyun.New concept of LoopInvariant and its application［EB/OL］.［2013-03-19］.http:∥link.springer.com/chapter/10.1007%2F11808107_1.

［15］Xue Jinyun.Two new strategies for developing loop invariants and their applications［J］.Journal of Computer Science and Technology，1993，8(2):147-154.

［16］Xue Jinyun.A unified approach for developing efficient algorithmic programs［J］.Journal of Computer Science and Technology，1997，12(4):314-329.

［17］Gries D.The science of programming［M］.New York:SpringerVerlag，1981.