程序正確性證明概述課件

第5章程序正確性證明5.1程序正確性驗證概述5.2不變式斷言法5.3子目標(biāo)斷言法5.4界函數(shù)法－－計數(shù)器法第5章程序正確性證明5.1程序正確性驗證概述15.1程序正確性概述什么樣的程序才是正確的？如何來保證程序是正確的？5.1程序正確性概述什么樣的程序才是正確的？2計算機(jī)程序是算法的一種精確描述，算法的任務(wù)是把給定的輸入信息變換為所需要的輸出信息。所謂一段程序是正確的，是指這段程序能準(zhǔn)確無誤地完成編寫者所期望賦予它的功能?；蛘哒f，對任何一組允許的輸入信息，程序執(zhí)行后能得到一組和這組輸入信息相對應(yīng)的正確的輸出信息。通俗地說，“做了它該做的事，沒有做它不該做的事”。結(jié)構(gòu)化程序的正確性驗證計算機(jī)程序是算法的一種精確描述，算法的任務(wù)是把給定的輸入信息3一段程序是錯誤的，是指：(1)程序完成的事情并不是程序員想要完成的事情；(2)程序員想要程序完成的事情，程序并沒有完成。一般來說，程序中含有錯誤是很難避免的錯誤可能有：（1）設(shè)計時的錯誤；（2）程序編寫時的錯誤；（3）運行時的錯誤等;……一段程序是錯誤的，是指：4如何發(fā)現(xiàn)錯誤或盡量減少錯誤？(1)設(shè)計程序時盡可能使用結(jié)構(gòu)化程序設(shè)計方法，使程序設(shè)計過程規(guī)范化和標(biāo)準(zhǔn)化；(2)程序調(diào)試或運行時采用測試的方法去跟蹤程序的運行，從而發(fā)現(xiàn)與改正錯誤；(3)利用程序正確性證明的方法檢驗程序是否正確。如何發(fā)現(xiàn)錯誤或盡量減少錯誤？51983年IEEE提出的軟件工程術(shù)語中給軟件測試下的定義是：“使用人工或者自動手段來運行或測定某個系統(tǒng)的過程，其目的在于檢驗它是否滿足規(guī)定的需求或是弄清預(yù)期結(jié)果與實際結(jié)果之間的差別?！睖y試是程序的執(zhí)行過程，目的在于發(fā)現(xiàn)錯誤。一個好的測試用例在于能發(fā)現(xiàn)至今未發(fā)現(xiàn)的錯誤；一個成功的測試是發(fā)現(xiàn)了至今未發(fā)現(xiàn)的錯誤的測試。1983年IEEE提出的軟件工程術(shù)語中給軟件測試下的定義是：6測試的原則1.應(yīng)當(dāng)“盡早地和不斷地進(jìn)行軟件測試”。2.測試用例應(yīng)由測試輸入數(shù)據(jù)和對應(yīng)的預(yù)期輸出結(jié)果組成。3.程序員應(yīng)避免檢查自己的程序。4.在設(shè)計測試用例時，應(yīng)當(dāng)包括合理的輸入條件和不合理的輸入條件。測試的原則1.應(yīng)當(dāng)“盡早地和不斷地進(jìn)行軟件測試”。75.充分注意測試中的群集現(xiàn)象。即測試后程序中殘存的錯誤數(shù)目與該程序中已發(fā)現(xiàn)的錯誤數(shù)目成正比。6.嚴(yán)格執(zhí)行測試計劃，排除測試的隨意性。7.應(yīng)當(dāng)對每一個測試結(jié)果做全面檢查。8.妥善保存測試計劃，測試用例，出錯統(tǒng)計和最終分析報告，為維護(hù)提供方便。5.充分注意測試中的群集現(xiàn)象。即測試后程序中殘存的錯誤數(shù)目8程序測試實質(zhì)上只是一種抽樣檢查測試過程：選取測試數(shù)據(jù)→執(zhí)行程序→輸入測試數(shù)據(jù)→記錄執(zhí)行結(jié)果→手工核對結(jié)果因此，測試只是一種查錯的手段，它可以幫助人們?nèi)グl(fā)現(xiàn)程序中的錯誤，但不能證明程序中沒有錯誤，即：測試不能證明程序是正確的程序測試實質(zhì)上只是一種抽樣檢查9測試只能發(fā)現(xiàn)程序錯誤，但不能證明程序無錯。原因：測試并沒有也不可能包含所有數(shù)據(jù)，只是選擇了一些具有代表性的數(shù)據(jù)，所以它具有局限性。正確性證明是通過數(shù)學(xué)技術(shù)來確定軟件是否正確，也就是說，是否符合其規(guī)格說明。測試只能發(fā)現(xiàn)程序錯誤，但不能證明程序無錯。10關(guān)于程序正確性的認(rèn)識什么樣的程序才是正確的？

“測試”或“調(diào)試”方法

根據(jù)問題的特性和軟件所要實現(xiàn)的功能，選擇一些具有代表性的數(shù)據(jù)，設(shè)計測試用例。通過用例程序執(zhí)行，去發(fā)現(xiàn)被測試程序的錯誤。

采用“測試”方法可以發(fā)現(xiàn)程序中的錯誤，但卻不能證明程序中沒有錯誤！因此，為保證程序的正確性，必須從理論上研究有關(guān)“程序正確性證明”的方法。關(guān)于程序正確性的認(rèn)識什么樣的程序才是正確的？采11程序正確性證明發(fā)展歷程20世紀(jì)50年代Turing開始研究。1967年，F(xiàn)loyd和Naur提出不變式斷言法。1969年，Hoare提出公理化方法。1975年，Dijkstra提出最弱前置謂詞和程序推導(dǎo)方法，解決了斷言構(gòu)造難的問題，可從程序規(guī)約推導(dǎo)出正確程序，使正確性證明變得實用。

程序正確性理論是十分活躍的課題，不僅可以證明順序程序的正確性，而且還可以證明非確定性程序，以及并行程序的正確性。程序正確性證明發(fā)展歷程20世紀(jì)50年代Turing開始研究12程序正確性理論程序設(shè)計的一般過程程序正確性理論程序設(shè)計的一般過程13程序正確性理論程序功能的精確描述1、程序規(guī)約：對程序所實現(xiàn)功能的精確描述，由程序的前置斷言和后置斷言兩部分組成。2、前置斷言：程序執(zhí)行前的輸入應(yīng)滿足的條件，又稱為輸入斷言。3、后置斷言：程序執(zhí)行后的輸出應(yīng)滿足的條件，又稱為輸出斷言。程序設(shè)計過程：問題程序規(guī)約程序程序正確性理論程序功能的精確描述程序設(shè)計過程：問題14程序規(guī)約的基本分類非形式化程序規(guī)約非形式化程序規(guī)約采用自然語言描述程序功能，簡單、方便，但存在二義性，因此，不利于程序的正確性證明。形式化程序規(guī)約采用數(shù)學(xué)化的語言描述程序功能，描述精確，無二義性，便于程序的正確性證明。程序規(guī)約的基本分類非形式化程序規(guī)約15程序規(guī)約的實例在書寫程序規(guī)約時，使用Q表示前置斷言，R表示后置斷言，S表示問題求解的實現(xiàn)程序。在前置斷言Q之前，還必須給出Q和R中所出現(xiàn)的標(biāo)識符的必要說明。例1：求數(shù)組b[0:n-1]中所有元素的最大值。[inn:integer;inb[0:n-1]:arrayofinteger;outy:integer]Q:{n≥1}SR:{y＝MAX(i:0≤i＜n;b[i])}程序規(guī)約的實例在書寫程序規(guī)約時，使用Q表示前置斷言，R表示后16程序規(guī)約的實例例2：求兩個非負(fù)整數(shù)的最大公約數(shù)。[ina,b:integer;outy:integer]Q:{a≥0∧b≥0}SR:{y＝MAX(i:1≤i≤min(a,b)∧(amodi＝0)∧(bmodi＝0))}程序規(guī)約的實例例2：求兩個非負(fù)整數(shù)的最大公約數(shù)。17程序正確性定義衡量一個程序的正確性，主要看程序是否實現(xiàn)了問題所要求的功能。若程序?qū)崿F(xiàn)了問題所要求的功能，則稱它為正確的，否則是不正確的。對程序的正確性理解，可以分為兩個層次：從廣義來說，一個程序的正確性取決于該程序滿足問題實際需求的程度。從狹義而言，如果一個程序滿足了它的程序規(guī)約就是正確的。程序設(shè)計過程：問題程序規(guī)約程序程序正確性定義衡量一個程序的正確性，主要看程序是否實現(xiàn)了問題18程序正確性定義程序規(guī)約Q{S}R是一個邏輯表達(dá)式，其取值為真或假。 其中取值為真的含義是指：給定一段程序S，若程序開始執(zhí)行之前Q為真，S的執(zhí)行將終止，且終止時R為真，則稱為“程序S，關(guān)于前置斷言Q和后置斷言R是完全正確的”。程序正確性定義程序規(guī)約Q{S}R是一個邏輯表達(dá)式，其取值為真19程序正確性定義部分正確： 若對于每個使得Q(i)為真，并且程序S計算終止的輸入信息i，R(i,S(i))都為真，則稱程序S關(guān)于Q和R是部分正確的。程序終止： 若對于每個使得Q(i)為真的輸入i，程序S的計算都終止，則稱程序S關(guān)于Q是終止的。完全正確： 若對于每個使得Q(i)為真的輸入信息i，程序S的計算都將終止，并且R(i,S(i))都為真，則稱程序S關(guān)于Q和R是完全正確的。一個程序的完全正確，等價于該程序是部分正確，同時又是終止的。程序正確性定義部分正確：20程序正確性的證明方法分類證明部分正確性的方法

A.Floyd的不變式斷言法

B.Manna的子目標(biāo)斷言法

C.Hoare的公理化方法終止性證明的方法

A.Floyd的良序集方法

B.Knuth的計數(shù)器方法

C.Manna等人的不動點方法完全正確性的方法

A.Hoare公理化方法的推廣

B.Burstall的間發(fā)斷言法

C.Dijkstra的弱謂詞變換方法以及強(qiáng)驗證方法程序正確性的證明方法分類證明部分正確性的方法21第5章程序正確性證明5.1程序正確性驗證概述5.2不變式斷言法5.3子目標(biāo)斷言法5.4界函數(shù)法－－計數(shù)器法第5章程序正確性證明5.1程序正確性驗證概述22循環(huán)不變式斷言把反映循環(huán)變量的變化規(guī)律，且在每次循環(huán)體的執(zhí)行前后均為真的邏輯表達(dá)式稱為該循環(huán)的不變式斷言。

例帶余整數(shù)除法問題：設(shè)x為非負(fù)整數(shù)，y為正整數(shù)，求x除以y的商q，以及余數(shù)r。

程序：q＝0；r＝x；while(r≥y)//該循環(huán)不變式斷言：{r＝r－y；q＝q＋1；}//(x＝y(tǒng)×q＋r)∧r≥0循環(huán)不變式斷言把反映循環(huán)變量的變化規(guī)律，且在每次循環(huán)體的執(zhí)行235.2不變式斷言法證明步驟：1、建立斷言 建立程序的輸入、輸出斷言，如果程序中有循環(huán)出現(xiàn)的話，在循環(huán)中選取一個斷點，在斷點處建立一個循環(huán)不變式斷言。2、建立檢驗條件 將程序分解為不同的通路，為每一個通路建立一個檢驗條件，該檢驗條件為如下形式：

I∧R=>O

其中I為輸入斷言，R為進(jìn)入通路的條件，O為輸出斷言。3、證明檢驗條件 運用數(shù)學(xué)工具證明步驟2得到的所有檢驗條件，如果每一條通路檢驗條件都為真，則該程序為部分正確的。5.2不變式斷言法證明步驟：24不變式斷言法實例1例：設(shè)x,y為正整數(shù)，求x,y的最大公約數(shù)z的程序，即z=gcd(x,y)。Functiongcd(x1,x2:integer);vary1,y2,z:Integer;Begin y1:=x1;y2:=x2; while(y1<>y2)do if(y1>y2)y1:=y1-y2elsey2:=y2-y1z:=y1;write(z);End.START(x1,x2)－>(y1,y2)y1<>y2y1>y2y1:=y1-y2y2:=y2-y1z:=y1STOPTFTF不變式斷言法實例1例：設(shè)x,y為正整數(shù)，求x,y的最大公約數(shù)25不變式斷言法實例1(建立斷言)輸入斷言： I(x1,x2):x1>0∧x2>0輸出斷言： O(x1,x2,z):z=gcd(x1,x2)循環(huán)不變式斷言： P(x1,x2,y1,y2): x1>0∧x2>0∧ y1>0∧y2>0∧ gcd(y1,y2)=gcd(x1,x2)

通路劃分：通路1：a->b通路2：b->d->b通路3：b->e->b通路4：b->g->cSTART(x1,x2)->(y1,y2)y1<>y2y1>y2y1:=y1-y2y2:=y2-y1z:=y1STOPTFTFI(x1,x2)aP(x1,x2,y1,y2)bcO(x1,x2,z)deg······不變式斷言法實例1(建立斷言)輸入斷言：通路劃分：ST26不變式斷言法實例1(建立檢驗條件)檢驗條件：I∧R=>O通路1：I(x1,x2)=>P(x1,x2,y1,y2)x1>0∧x2>0=>

x1>0∧x2>0∧y1>0∧Y2>0∧gcd(y1,y2)=gcd(x1,x2)通路2：P(x1,x2,y1,y2)∧y1<>y2∧y1>y2=>P(x1,x2,y1-y2,y2)x1>0∧x2>0∧y1>0∧y2>0∧gcd(y1,y2)=gcd(x1,x2)∧y1<>y2∧y1>y2=>x1>0∧x2>0∧y1-y2>0∧y2>0∧gcd(y1-y2,y2)=gcd(x1,x2)不變式斷言法實例1(建立檢驗條件)檢驗條件：I∧R=27不變式斷言法實例1(建立檢驗條件)通路3：P(x1,x2,y1,y2)∧y1<>y2∧y1<y2=>P(x1,x2,y1,y2-y1)x1>0∧x2>0∧y1>0∧y2>0∧gcd(y1,y2)=gcd(x1,x2)∧y1<>y2∧y1<y2=>x1>0∧x2>0∧y1>0∧y2-y1>0∧gcd(y1,y2-y1)=gcd(x1,x2)通路4：P(x1,x2,y1,y2)∧y1=y2=>O(x1,x2,z)x1>0∧x2>0∧y1>0∧y2>0∧gcd(y1,y2)=gcd(x1,x2)∧y1=y2=>z=gcd(x1,x2)不變式斷言法實例1(建立檢驗條件)通路3：28不變式斷言法實例1(證明檢驗條件)通路1： x1>0∧x2>0∧x1=y1∧x2=y2=>……通路2：

若y1>y2,gcd(y1-y2,y2)=gcd(y1,y2)=gcd(x1,x2)通路3:

若y2>y1,gcd(y1,y2)=gcd(y1,y2-y1)=gcd(x1,x2)通路4:

若y1=y2,gcd(y1,y2)=gcd(x1,x2)=y1=y2=zP(x1,x2,y1,y2)∧y1=y2=>O(x1,x2,z)不變式斷言法實例1(證明檢驗條件)通路1：29不變式斷言法實例2對任一給定的自然數(shù)x，計算z＝[]，即計算x的平方根取整。1＋3＋…(2n+1)=(n+1)2y1=n;y3=2×y1+1;y2=(y1+1)2輸入斷言：I(x):x>0輸出斷言：O(x,z):z2≤x<(z+1)2循環(huán)不變式：P(x,y1,y2,y3)：y12≤x∧y2=(y1+1)2

∧y3=2y1+1開始(0,0,1)－>(y1,y2,y3)y2+y3－>y2y2≤x(y1+1,y3+2)－>(y1,y3)y1－>z結(jié)束AI(x)BP(x,y1,y2,y3)DCO(x,z)FT····不變式斷言法實例2對任一給定的自然數(shù)x，計算z＝[30不變式斷言法實例2檢驗條件：I∧R=>O通路1：A->BI(x)=>P(x,0,1,1)x>0=>0≤x∧1=(0+1)2∧1=2*0+1通路2：B->D->BP(x,y1,y2,y3)∧y2≤x=>p(x,y1+1,y2+y3+2,y3+2)y12≤x∧y2=(y1+1)2∧y3=2y1+1∧y2≤x=>(y1+1)2≤x∧y2+y3+2=(y1+1+1)2∧y3+2=2(y1+1)+1通路3：B->CP(x,y1,y2,y3)∧y2>x=>O(x,y1)y12≤x∧y2=(y1+1)2∧y3=2y1+1∧y2>x=>

y12≤x<(y1+1)2不變式斷言法實例2檢驗條件：I∧R=>O31不變式斷言法實例2檢驗條件2y12≤x∧y2=(y1+1)2∧y3=2y1+1∧y2≤x=>(y1+1)2≤x∧y2+y3+2=(y1+1+1)2∧y3+2=2(y1+1)+1證明：x≥(y1+1)2——(y2≤x,y2=(y1+1)2

)y2+y3+2=(y1+1)2+2y1+1+2 =(y1+1)2+2(y1+1)+1=(y1+1+1)2y3+2=2y1+1+2=2(y1+1)+1檢驗條件3y12≤x∧y2=(y1+1)2∧y3=2y1+1∧y2>x=>y12≤x<(y1+1)2

證明：y12≤xx<y2,y2=(y1+1)2=>x<(y1+1)2不變式斷言法實例2檢驗條件232作業(yè)課本P174習(xí)題1、習(xí)題2。要求用不變式斷言法證明。作業(yè)課本P174習(xí)題1、習(xí)題2。要求用不變式斷言法證明。33第5章程序正確性證明5.1程序正確性驗證概述5.2不變式斷言法5.3子目標(biāo)斷言法5.4界函數(shù)法－－計數(shù)器法第5章程序正確性證明5.1程序正確性驗證概述345.3子目標(biāo)斷言法子目標(biāo)斷言法與不變式斷言法的主要區(qū)別是：兩種方法對循環(huán)所建立的斷言不同。不變式斷言描述了程序變量y的中間值與初始值之間關(guān)系；子目標(biāo)斷言法描述的是y的中間值與循環(huán)終止時的最終值yend之間的關(guān)系。兩種方法進(jìn)行歸納的方向不同。不變式斷言沿著程序正常執(zhí)行的方向進(jìn)行歸納；子目標(biāo)斷言法則沿著相反方向進(jìn)行歸納。5.3子目標(biāo)斷言法子目標(biāo)斷言法與不變式斷言法的主要區(qū)別是：35不變式斷言法輸入斷言： I(x,y):x0>=0∧y0>=0輸出斷言： O(x,y,z):z=gcd(x,y)循環(huán)不變式斷言：P(x,y):x>=0∧y>=0∧ gcd(x,y)=gcd(x0,y0)例：設(shè)x,y為非負(fù)整數(shù)，求x,y的最大公約數(shù)z的程序，即z=gcd(x,y)。STARTRead(x,y)x<>0y>=xy:=y-xxyz:=ySTOPTFTFI(x,y)aP(x,y)bcO(x,y,z)deg······不變式斷言法輸入斷言：例：設(shè)x,y為非負(fù)整數(shù)，求x,y的最大36子目標(biāo)斷言法(建立斷言)輸入斷言

I(x,y):x0>=0∧

y0>=0∧(x0≠0∨y0≠0)輸出斷言O(shè)(x,y,z):z=gcd(x,y)子目標(biāo)斷言P(x,y,yend):x>=0∧y>=0∧(x≠0∨y≠0)

=>yend=gcd(x,y)STARTRead(x,y)x<>0y>=xy:=y-xxyz:=ySTOPTFTFI(x,y)aP(x,y,yend)bcO(x,y,z)deg······子目標(biāo)斷言法(建立斷言)輸入斷言STARTRe37子目標(biāo)斷言法(建立檢驗條件)通路1： 控制轉(zhuǎn)出循環(huán)時，子目標(biāo)斷言成立。通路2、通路3： 如果在通過循環(huán)之后，子目標(biāo)斷言在斷點處成立，那么，在通過循環(huán)之前，斷言也成立。通路4： 如果輸入斷言為真，且控制第一次通過斷點B時子目標(biāo)斷言為真，則輸出斷言為真。子目標(biāo)斷言法(建立檢驗條件)通路1：38子目標(biāo)斷言法(建立檢驗條件)通路1：b->c檢驗條件1

x=0=>P(x,y,yend)x=0=>

[x>=0∧y>=0∧

(x≠0∨y≠0)

=> yend=gcd(x,y)]

通路2：b->d->b檢驗條件2P(x,y-x,yend)∧x<>0∧y>=x=>P(x,y,yend)[x>=0∧y-x>=0∧

(x≠0∨y-x≠0)

=>yend=gcd(x,y-x)]∧x<>0∧y>=x=>

[x>=0∧y>=0∧(x≠0∨y≠0)

=>yend=gcd(x,y)]通路3：b->e->b檢驗條件3P(y,x,yend)∧x<>0∧y<x=>P(x,y,yend)通路4：a->b檢驗條件4x0>=0∧

y0>=0∧

(x0

≠0∨y0

≠0)

∧P(x0,y0,yend)=>yend=gcd(x0,y0)子目標(biāo)斷言法(建立檢驗條件)通路1：b->c39子目標(biāo)斷言法(證明檢驗條件)檢驗條件1： x=0=>[x>=0∧y>=0=>yend=gcd(x,y)]證明： 因為有x=0,yend=y 所以yend=y=gcd(0,y)=gcd(x,y)檢驗條件2：P(x,y-x,yend)∧x<>0∧y>x=>P(x,y,yend)即證明：[

x>=0∧y-x>=0∧(x≠0∨y-x≠0)=>

yend=gcd(x,y-x)]∧x<>0∧y>=x=>

[x>=0∧y>=0∧(x≠0∨y≠0)=>

yend=gcd(x,y)]

子目標(biāo)斷言法(證明檢驗條件)檢驗條件1：40程序部分正確但不終止實例例：求兩個非負(fù)整數(shù)x、y的最大公約數(shù)z的程序。ProgramAvarx,y,z,s:integer;beginread(x,y);whilex≠0doify>xtheny=y–x;elsex=x–y;z=y;write(z);end.STARTRead(x,y)x≠0y>xy:=y-xx:=x-yz:=ySTOPTFTFI(x,y)aP(x,y)bcO(x,y,z)deg······可以利用不變式斷言等方法證明該程序的部分正確性，但無法證明它是終止的。因為當(dāng)y＝0時，程序循環(huán)將不終止！

程序部分正確但不終止實例例：求兩個非負(fù)整數(shù)x、y的最大公約數(shù)41第5章程序正確性證明5.1程序正確性驗證概述5.2不變式斷言法5.3子目標(biāo)斷言法5.4界函數(shù)法－－計數(shù)器法第5章程序正確性證明5.1程序正確性驗證概述425.4計數(shù)器方法證明程序終止性證明思路 通過估計循環(huán)執(zhí)行的最大次數(shù)證明程序終止性的方法。證明步驟:1.為程序的每一個循環(huán)附加一個新的變量作為該循環(huán)的計數(shù)器，初始值置為0，每循環(huán)一次該計數(shù)器加1。2.為每個循環(huán)設(shè)置一個中間斷言，它表示相應(yīng)的計數(shù)器不會超過固定的界限。3.證明（2）中的中間斷言是不變式斷言。5.4計數(shù)器方法證明程序終止性證明思路43計數(shù)器方法證明程序終止性實例計算非負(fù)整數(shù)的最大公約數(shù)varx,y,z,s:integer;beginRead(x,y)whilex≠0dobeginIfy≥xthen y:=y-x;else s:=x;x:=y;y:=s;endz:=y;write(z);endSTARTRead(x,y)x≠0y≥xy:=y-xxyz:=ySTOPTFTFI(x,y)aP(x,y)bO(x,y)de····c·計數(shù)器方法證明程序終止性實例計算非負(fù)整數(shù)的最大公約數(shù)var44計數(shù)器方法證明程序終止性實例1.引進(jìn)計數(shù)器I,并建立如下斷言

x≥0∧y≥0∧2x+y+I≤2x0+y0

varx,y,z,s:integer;read(x,y);I:=0;//計數(shù)器賦初值whilex≠0dobeginify≥xtheny:=y-x; elses:=x;x:=y;y:=sfi;I:=I+1;//計數(shù)器遞增End;z:=y;write(z);計數(shù)器方法證明程序終止性實例1.引進(jìn)計數(shù)器I,并建立如下斷言45計數(shù)器方法證明程序終止性實例2.建立檢驗條件并證明，從而證明計數(shù)器斷言為不變式斷言。檢驗條件1：a->b [x0≥0∧y0≥0]=>[x0≥0∧y0≥0∧2x0+y0+0≤2x0+y0]檢驗條件2：b->d->b[x≥0∧y≥0∧(2x+y+I≤2x0+y0)∧x≠0∧y≥x]=>[x≥0∧y-x≥0∧(2x+(y-x)+I+1≤2x0+y0)]證明：x≠0=>(x-1≥0)

∴

2x+(y-x)+I+1=2x+y+I-(x-1)≤2x+y+I≤2x0+y0檢驗條件3：b->e->b[x≥0∧y≥0∧(2x+y+I≤2x0+y0)∧x≠0∧y<x]=>[y≥0∧x≥0∧(2y+x+I+1≤2x0+y0)]證明：(y<x∧x≠0=>y≤x-1)

∴

2y+x+I+1≤y+x-1+x+I+1=y+2x+I≤2x0+y0由于2x+y+I≤2x0+y0是不變式斷言，因此，I（循環(huán)次數(shù)）必定小于常量2x0+y0，也就是循環(huán)只能執(zhí)行有限次，即程序終止。采用計數(shù)器方法證明程序終止性和利用不變式斷言法證明部分正確性步驟完全類似，只要再添加輸出斷言部分檢驗條件并證明，即可完成程序部分正確性證明。因此，可以把上述兩者聯(lián)合起來，完成程序的完全正確性證明。

計數(shù)器方法證明程序終止性實例2.建立檢驗條件并證明，從而證明465.4界函數(shù)法－－計數(shù)器方法的變形該方法是計數(shù)器方法的一種變形，證明程序的可終止性的常用方法.界函數(shù)法:對程序中的每一個循環(huán),構(gòu)造一個界函數(shù),若該循環(huán)存在界函數(shù),則該循環(huán)是可終止的,否則,該循環(huán)不可終止.界函數(shù)必須滿足的條件:(1)與循環(huán)變量有關(guān)的整函數(shù),記為N(x,y);(2)在循環(huán)的過程中N(x,y)>0;(3)每執(zhí)行一次循環(huán),N(x,y)的值減小.5.4界函數(shù)法－－計數(shù)器方法的變形該方法是計數(shù)器方法的一種473.4界函數(shù)法－－計數(shù)器法例3.證明例1的可終止性.y1:=x1,y2:=x2y1<>y2y1>y2z:=y1y2:=y2-y1y1:=y1-y2ABCDEFTFT取N(x,y)=max(y1,y2)3.4界函數(shù)法－－計數(shù)器法例3.證明例1的可終止性.y1:=483.4界函數(shù)法－－計數(shù)器法因為x1>0^x2>0,所以循環(huán)第一次進(jìn)入循環(huán)時y1>0^y2>0.進(jìn)入循環(huán)以后,當(dāng)y1>y2時,y1=y1-y2>0,y2不變,所以N(x,y)>0.當(dāng)y1<y2時,y2=y2-y1>0,y1不變,所以N(x,y)>0.故在循環(huán)過程中N(x,y)>0;當(dāng)y1>y2時,N(y1-y2,y2)<N(y1,y2)當(dāng)y1<y2時,N(y1,y2-y1)<N(y1,y2)故隨著循環(huán)的執(zhí)行,N(x,y)遞減.故該循環(huán)存在界函數(shù)N(x,y)=max(y1,y2),所以該循環(huán)可終止.3.4界函數(shù)法－－計數(shù)器法因為x1>0^x2>0,所以循環(huán)第49另一種計數(shù)器方法證明程序終止性證明思路： 對程序中的每一個循環(huán)，構(gòu)造一個和該循環(huán)中變量有關(guān)的整數(shù)函數(shù)N(x,y)，若N(x,y)滿足以下兩個條件：當(dāng)循環(huán)條件成立時，N(x,y)>0；每次循環(huán)，N(x,y)都減小。 由N(x,y)的值構(gòu)成一個單調(diào)遞減的整數(shù)序列，N(x,y)>0，因而，循環(huán)只能執(zhí)行有限次。另一種計數(shù)器方法證明程序終止性證明思路：50另一種計數(shù)器方法證明程序終止性實例例：設(shè)x,y為正整數(shù)，求x,y的最大公約數(shù)z的程序，即z=gcd(x,y)。START(x1,x2)－>(y1,y2)y1≠y2y1>y2y1:=y1－y2y2:=y2－y1z:=y1STOPTFTF另一種計數(shù)器方法證明程序終止性實例例：設(shè)x,y為正整數(shù)，求x51另一種計數(shù)器方法證明程序終止性實例選取N(y1,y2)=max(y1,y2)輸入斷言：

I(x1,x2):x1>0∧x2>0當(dāng)?shù)谝淮芜M(jìn)入循環(huán)時有

y1>0∧y2>0有算法得y1>y2,則y1-y2－>y1,y2不變；y1<y2,則y2-y1－>y2,y1不變?！嗍冀K有y1>0∧y2>0于是就有N(y1,y2)>0;每執(zhí)行一次循環(huán)，N(y1,y2)是遞減的。START(x1,x2)->(y1,y2)y1≠y2y1>y2y1:=y1-y2y2:=y2-y1z:=y1STOPTFTF另一種計數(shù)器方法證明程序終止性實例選取N(y1,y2)=52采用計數(shù)器方法證明程序終止性難點采用計數(shù)器方法證明程序終止性關(guān)鍵在于確定一個合適的中間斷言（或選取一個合適的函數(shù)N（x,y）），尤其對于一些循環(huán)次數(shù)事先難以估計的程序，要找出循環(huán)次數(shù)的上限更為困難。采用計數(shù)器方法證明程序終止性難點采用計數(shù)器方法證明程序終止性53正整數(shù)的一個性質(zhì)對于任意正整數(shù)，滿足下列關(guān)系：若y1>y2,gcd(y1,y2)=gcd(y1-y2,y2)若y2>y1,gcd(y1,y2)=gcd(y1,y2-y1)若y1=y2,gcd(y1,y2)=y1=y2正整數(shù)的一個性質(zhì)對于任意正整數(shù)，滿足下列關(guān)系：54演講完畢，謝謝觀看！演講完畢，謝謝觀看！55第5章程序正確性證明5.1程序正確性驗證概述5.2不變式斷言法5.3子目標(biāo)斷言法5.4界函數(shù)法－－計數(shù)器法第5章程序正確性證明5.1程序正確性驗證概述565.1程序正確性概述什么樣的程序才是正確的？如何來保證程序是正確的？5.1程序正確性概述什么樣的程序才是正確的？57計算機(jī)程序是算法的一種精確描述，算法的任務(wù)是把給定的輸入信息變換為所需要的輸出信息。所謂一段程序是正確的，是指這段程序能準(zhǔn)確無誤地完成編寫者所期望賦予它的功能?；蛘哒f，對任何一組允許的輸入信息，程序執(zhí)行后能得到一組和這組輸入信息相對應(yīng)的正確的輸出信息。通俗地說，“做了它該做的事，沒有做它不該做的事”。結(jié)構(gòu)化程序的正確性驗證計算機(jī)程序是算法的一種精確描述，算法的任務(wù)是把給定的輸入信息58一段程序是錯誤的，是指：(1)程序完成的事情并不是程序員想要完成的事情；(2)程序員想要程序完成的事情，程序并沒有完成。一般來說，程序中含有錯誤是很難避免的錯誤可能有：（1）設(shè)計時的錯誤；（2）程序編寫時的錯誤；（3）運行時的錯誤等;……一段程序是錯誤的，是指：59如何發(fā)現(xiàn)錯誤或盡量減少錯誤？(1)設(shè)計程序時盡可能使用結(jié)構(gòu)化程序設(shè)計方法，使程序設(shè)計過程規(guī)范化和標(biāo)準(zhǔn)化；(2)程序調(diào)試或運行時采用測試的方法去跟蹤程序的運行，從而發(fā)現(xiàn)與改正錯誤；(3)利用程序正確性證明的方法檢驗程序是否正確。如何發(fā)現(xiàn)錯誤或盡量減少錯誤？601983年IEEE提出的軟件工程術(shù)語中給軟件測試下的定義是：“使用人工或者自動手段來運行或測定某個系統(tǒng)的過程，其目的在于檢驗它是否滿足規(guī)定的需求或是弄清預(yù)期結(jié)果與實際結(jié)果之間的差別?！睖y試是程序的執(zhí)行過程，目的在于發(fā)現(xiàn)錯誤。一個好的測試用例在于能發(fā)現(xiàn)至今未發(fā)現(xiàn)的錯誤；一個成功的測試是發(fā)現(xiàn)了至今未發(fā)現(xiàn)的錯誤的測試。1983年IEEE提出的軟件工程術(shù)語中給軟件測試下的定義是：61測試的原則1.應(yīng)當(dāng)“盡早地和不斷地進(jìn)行軟件測試”。2.測試用例應(yīng)由測試輸入數(shù)據(jù)和對應(yīng)的預(yù)期輸出結(jié)果組成。3.程序員應(yīng)避免檢查自己的程序。4.在設(shè)計測試用例時，應(yīng)當(dāng)包括合理的輸入條件和不合理的輸入條件。測試的原則1.應(yīng)當(dāng)“盡早地和不斷地進(jìn)行軟件測試”。625.充分注意測試中的群集現(xiàn)象。即測試后程序中殘存的錯誤數(shù)目與該程序中已發(fā)現(xiàn)的錯誤數(shù)目成正比。6.嚴(yán)格執(zhí)行測試計劃，排除測試的隨意性。7.應(yīng)當(dāng)對每一個測試結(jié)果做全面檢查。8.妥善保存測試計劃，測試用例，出錯統(tǒng)計和最終分析報告，為維護(hù)提供方便。5.充分注意測試中的群集現(xiàn)象。即測試后程序中殘存的錯誤數(shù)目63程序測試實質(zhì)上只是一種抽樣檢查測試過程：選取測試數(shù)據(jù)→執(zhí)行程序→輸入測試數(shù)據(jù)→記錄執(zhí)行結(jié)果→手工核對結(jié)果因此，測試只是一種查錯的手段，它可以幫助人們?nèi)グl(fā)現(xiàn)程序中的錯誤，但不能證明程序中沒有錯誤，即：測試不能證明程序是正確的程序測試實質(zhì)上只是一種抽樣檢查64測試只能發(fā)現(xiàn)程序錯誤，但不能證明程序無錯。原因：測試并沒有也不可能包含所有數(shù)據(jù)，只是選擇了一些具有代表性的數(shù)據(jù)，所以它具有局限性。正確性證明是通過數(shù)學(xué)技術(shù)來確定軟件是否正確，也就是說，是否符合其規(guī)格說明。測試只能發(fā)現(xiàn)程序錯誤，但不能證明程序無錯。65關(guān)于程序正確性的認(rèn)識什么樣的程序才是正確的？

“測試”或“調(diào)試”方法

根據(jù)問題的特性和軟件所要實現(xiàn)的功能，選擇一些具有代表性的數(shù)據(jù)，設(shè)計測試用例。通過用例程序執(zhí)行，去發(fā)現(xiàn)被測試程序的錯誤。

采用“測試”方法可以發(fā)現(xiàn)程序中的錯誤，但卻不能證明程序中沒有錯誤！因此，為保證程序的正確性，必須從理論上研究有關(guān)“程序正確性證明”的方法。關(guān)于程序正確性的認(rèn)識什么樣的程序才是正確的？采66程序正確性證明發(fā)展歷程20世紀(jì)50年代Turing開始研究。1967年，F(xiàn)loyd和Naur提出不變式斷言法。1969年，Hoare提出公理化方法。1975年，Dijkstra提出最弱前置謂詞和程序推導(dǎo)方法，解決了斷言構(gòu)造難的問題，可從程序規(guī)約推導(dǎo)出正確程序，使正確性證明變得實用。

程序正確性理論是十分活躍的課題，不僅可以證明順序程序的正確性，而且還可以證明非確定性程序，以及并行程序的正確性。程序正確性證明發(fā)展歷程20世紀(jì)50年代Turing開始研究67程序正確性理論程序設(shè)計的一般過程程序正確性理論程序設(shè)計的一般過程68程序正確性理論程序功能的精確描述1、程序規(guī)約：對程序所實現(xiàn)功能的精確描述，由程序的前置斷言和后置斷言兩部分組成。2、前置斷言：程序執(zhí)行前的輸入應(yīng)滿足的條件，又稱為輸入斷言。3、后置斷言：程序執(zhí)行后的輸出應(yīng)滿足的條件，又稱為輸出斷言。程序設(shè)計過程：問題程序規(guī)約程序程序正確性理論程序功能的精確描述程序設(shè)計過程：問題69程序規(guī)約的基本分類非形式化程序規(guī)約非形式化程序規(guī)約采用自然語言描述程序功能，簡單、方便，但存在二義性，因此，不利于程序的正確性證明。形式化程序規(guī)約采用數(shù)學(xué)化的語言描述程序功能，描述精確，無二義性，便于程序的正確性證明。程序規(guī)約的基本分類非形式化程序規(guī)約70程序規(guī)約的實例在書寫程序規(guī)約時，使用Q表示前置斷言，R表示后置斷言，S表示問題求解的實現(xiàn)程序。在前置斷言Q之前，還必須給出Q和R中所出現(xiàn)的標(biāo)識符的必要說明。例1：求數(shù)組b[0:n-1]中所有元素的最大值。[inn:integer;inb[0:n-1]:arrayofinteger;outy:integer]Q:{n≥1}SR:{y＝MAX(i:0≤i＜n;b[i])}程序規(guī)約的實例在書寫程序規(guī)約時，使用Q表示前置斷言，R表示后71程序規(guī)約的實例例2：求兩個非負(fù)整數(shù)的最大公約數(shù)。[ina,b:integer;outy:integer]Q:{a≥0∧b≥0}SR:{y＝MAX(i:1≤i≤min(a,b)∧(amodi＝0)∧(bmodi＝0))}程序規(guī)約的實例例2：求兩個非負(fù)整數(shù)的最大公約數(shù)。72程序正確性定義衡量一個程序的正確性，主要看程序是否實現(xiàn)了問題所要求的功能。若程序?qū)崿F(xiàn)了問題所要求的功能，則稱它為正確的，否則是不正確的。對程序的正確性理解，可以分為兩個層次：從廣義來說，一個程序的正確性取決于該程序滿足問題實際需求的程度。從狹義而言，如果一個程序滿足了它的程序規(guī)約就是正確的。程序設(shè)計過程：問題程序規(guī)約程序程序正確性定義衡量一個程序的正確性，主要看程序是否實現(xiàn)了問題73程序正確性定義程序規(guī)約Q{S}R是一個邏輯表達(dá)式，其取值為真或假。 其中取值為真的含義是指：給定一段程序S，若程序開始執(zhí)行之前Q為真，S的執(zhí)行將終止，且終止時R為真，則稱為“程序S，關(guān)于前置斷言Q和后置斷言R是完全正確的”。程序正確性定義程序規(guī)約Q{S}R是一個邏輯表達(dá)式，其取值為真74程序正確性定義部分正確： 若對于每個使得Q(i)為真，并且程序S計算終止的輸入信息i，R(i,S(i))都為真，則稱程序S關(guān)于Q和R是部分正確的。程序終止： 若對于每個使得Q(i)為真的輸入i，程序S的計算都終止，則稱程序S關(guān)于Q是終止的。完全正確： 若對于每個使得Q(i)為真的輸入信息i，程序S的計算都將終止，并且R(i,S(i))都為真，則稱程序S關(guān)于Q和R是完全正確的。一個程序的完全正確，等價于該程序是部分正確，同時又是終止的。程序正確性定義部分正確：75程序正確性的證明方法分類證明部分正確性的方法

A.Floyd的不變式斷言法

B.Manna的子目標(biāo)斷言法

C.Hoare的公理化方法終止性證明的方法

A.Floyd的良序集方法

B.Knuth的計數(shù)器方法

C.Manna等人的不動點方法完全正確性的方法

A.Hoare公理化方法的推廣

B.Burstall的間發(fā)斷言法

C.Dijkstra的弱謂詞變換方法以及強(qiáng)驗證方法程序正確性的證明方法分類證明部分正確性的方法76第5章程序正確性證明5.1程序正確性驗證概述5.2不變式斷言法5.3子目標(biāo)斷言法5.4界函數(shù)法－－計數(shù)器法第5章程序正確性證明5.1程序正確性驗證概述77循環(huán)不變式斷言把反映循環(huán)變量的變化規(guī)律，且在每次循環(huán)體的執(zhí)行前后均為真的邏輯表達(dá)式稱為該循環(huán)的不變式斷言。

例帶余整數(shù)除法問題：設(shè)x為非負(fù)整數(shù)，y為正整數(shù)，求x除以y的商q，以及余數(shù)r。

程序：q＝0；r＝x；while(r≥y)//該循環(huán)不變式斷言：{r＝r－y；q＝q＋1；}//(x＝y(tǒng)×q＋r)∧r≥0循環(huán)不變式斷言把反映循環(huán)變量的變化規(guī)律，且在每次循環(huán)體的執(zhí)行785.2不變式斷言法證明步驟：1、建立斷言 建立程序的輸入、輸出斷言，如果程序中有循環(huán)出現(xiàn)的話，在循環(huán)中選取一個斷點，在斷點處建立一個循環(huán)不變式斷言。2、建立檢驗條件 將程序分解為不同的通路，為每一個通路建立一個檢驗條件，該檢驗條件為如下形式：

I∧R=>O

其中I為輸入斷言，R為進(jìn)入通路的條件，O為輸出斷言。3、證明檢驗條件 運用數(shù)學(xué)工具證明步驟2得到的所有檢驗條件，如果每一條通路檢驗條件都為真，則該程序為部分正確的。5.2不變式斷言法證明步驟：79不變式斷言法實例1例：設(shè)x,y為正整數(shù)，求x,y的最大公約數(shù)z的程序，即z=gcd(x,y)。Functiongcd(x1,x2:integer);vary1,y2,z:Integer;Begin y1:=x1;y2:=x2; while(y1<>y2)do if(y1>y2)y1:=y1-y2elsey2:=y2-y1z:=y1;write(z);End.START(x1,x2)－>(y1,y2)y1<>y2y1>y2y1:=y1-y2y2:=y2-y1z:=y1STOPTFTF不變式斷言法實例1例：設(shè)x,y為正整數(shù)，求x,y的最大公約數(shù)80不變式斷言法實例1(建立斷言)輸入斷言： I(x1,x2):x1>0∧x2>0輸出斷言： O(x1,x2,z):z=gcd(x1,x2)循環(huán)不變式斷言： P(x1,x2,y1,y2): x1>0∧x2>0∧ y1>0∧y2>0∧ gcd(y1,y2)=gcd(x1,x2)

通路劃分：通路1：a->b通路2：b->d->b通路3：b->e->b通路4：b->g->cSTART(x1,x2)->(y1,y2)y1<>y2y1>y2y1:=y1-y2y2:=y2-y1z:=y1STOPTFTFI(x1,x2)aP(x1,x2,y1,y2)bcO(x1,x2,z)deg······不變式斷言法實例1(建立斷言)輸入斷言：通路劃分：ST81不變式斷言法實例1(建立檢驗條件)檢驗條件：I∧R=>O通路1：I(x1,x2)=>P(x1,x2,y1,y2)x1>0∧x2>0=>

x1>0∧x2>0∧y1>0∧Y2>0∧gcd(y1,y2)=gcd(x1,x2)通路2：P(x1,x2,y1,y2)∧y1<>y2∧y1>y2=>P(x1,x2,y1-y2,y2)x1>0∧x2>0∧y1>0∧y2>0∧gcd(y1,y2)=gcd(x1,x2)∧y1<>y2∧y1>y2=>x1>0∧x2>0∧y1-y2>0∧y2>0∧gcd(y1-y2,y2)=gcd(x1,x2)不變式斷言法實例1(建立檢驗條件)檢驗條件：I∧R=82不變式斷言法實例1(建立檢驗條件)通路3：P(x1,x2,y1,y2)∧y1<>y2∧y1<y2=>P(x1,x2,y1,y2-y1)x1>0∧x2>0∧y1>0∧y2>0∧gcd(y1,y2)=gcd(x1,x2)∧y1<>y2∧y1<y2=>x1>0∧x2>0∧y1>0∧y2-y1>0∧gcd(y1,y2-y1)=gcd(x1,x2)通路4：P(x1,x2,y1,y2)∧y1=y2=>O(x1,x2,z)x1>0∧x2>0∧y1>0∧y2>0∧gcd(y1,y2)=gcd(x1,x2)∧y1=y2=>z=gcd(x1,x2)不變式斷言法實例1(建立檢驗條件)通路3：83不變式斷言法實例1(證明檢驗條件)通路1： x1>0∧x2>0∧x1=y1∧x2=y2=>……通路2：

若y1>y2,gcd(y1-y2,y2)=gcd(y1,y2)=gcd(x1,x2)通路3:

若y2>y1,gcd(y1,y2)=gcd(y1,y2-y1)=gcd(x1,x2)通路4:

若y1=y2,gcd(y1,y2)=gcd(x1,x2)=y1=y2=zP(x1,x2,y1,y2)∧y1=y2=>O(x1,x2,z)不變式斷言法實例1(證明檢驗條件)通路1：84不變式斷言法實例2對任一給定的自然數(shù)x，計算z＝[]，即計算x的平方根取整。1＋3＋…(2n+1)=(n+1)2y1=n;y3=2×y1+1;y2=(y1+1)2輸入斷言：I(x):x>0輸出斷言：O(x,z):z2≤x<(z+1)2循環(huán)不變式：P(x,y1,y2,y3)：y12≤x∧y2=(y1+1)2

∧y3=2y1+1開始(0,0,1)－>(y1,y2,y3)y2+y3－>y2y2≤x(y1+1,y3+2)－>(y1,y3)y1－>z結(jié)束AI(x)BP(x,y1,y2,y3)DCO(x,z)FT····不變式斷言法實例2對任一給定的自然數(shù)x，計算z＝[85不變式斷言法實例2檢驗條件：I∧R=>O通路1：A->BI(x)=>P(x,0,1,1)x>0=>0≤x∧1=(0+1)2∧1=2*0+1通路2：B->D->BP(x,y1,y2,y3)∧y2≤x=>p(x,y1+1,y2+y3+2,y3+2)y12≤x∧y2=(y1+1)2∧y3=2y1+1∧y2≤x=>(y1+1)2≤x∧y2+y3+2=(y1+1+1)2∧y3+2=2(y1+1)+1通路3：B->CP(x,y1,y2,y3)∧y2>x=>O(x,y1)y12≤x∧y2=(y1+1)2∧y3=2y1+1∧y2>x=>

y12≤x<(y1+1)2不變式斷言法實例2檢驗條件：I∧R=>O86不變式斷言法實例2檢驗條件2y12≤x∧y2=(y1+1)2∧y3=2y1+1∧y2≤x=>(y1+1)2≤x∧y2+y3+2=(y1+1+1)2∧y3+2=2(y1+1)+1證明：x≥(y1+1)2——(y2≤x,y2=(y1+1)2

)y2+y3+2=(y1+1)2+2y1+1+2 =(y1+1)2+2(y1+1)+1=(y1+1+1)2y3+2=2y1+1+2=2(y1+1)+1檢驗條件3y12≤x∧y2=(y1+1)2∧y3=2y1+1∧y2>x=>y12≤x<(y1+1)2

證明：y12≤xx<y2,y2=(y1+1)2=>x<(y1+1)2不變式斷言法實例2檢驗條件287作業(yè)課本P174習(xí)題1、習(xí)題2。要求用不變式斷言法證明。作業(yè)課本P174習(xí)題1、習(xí)題2。要求用不變式斷言法證明。88第5章程序正確性證明5.1程序正確性驗證概述5.2不變式斷言法5.3子目標(biāo)斷言法5.4界函數(shù)法－－計數(shù)器法第5章程序正確性證明5.1程序正確性驗證概述895.3子目標(biāo)斷言法子目標(biāo)斷言法與不變式斷言法的主要區(qū)別是：兩種方法對循環(huán)所建立的斷言不同。不變式斷言描述了程序變量y的中間值與初始值之間關(guān)系；子目標(biāo)斷言法描述的是y的中間值與循環(huán)終止時的最終值yend之間的關(guān)系。兩種方法進(jìn)行歸納的方向不同。不變式斷言沿著程序正常執(zhí)行的方向進(jìn)行歸納；子目標(biāo)斷言法則沿著相反方向進(jìn)行歸納。5.3子目標(biāo)斷言法子目標(biāo)斷言法與不變式斷言法的主要區(qū)別是：90不變式斷言法輸入斷言： I(x,y):x0>=0∧y0>=0輸出斷言： O(x,y,z):z=gcd(x,y)循環(huán)不變式斷言：P(x,y):x>=0∧y>=0∧ gcd(x,y)=gcd(x0,y0)例：設(shè)x,y為非負(fù)整數(shù)，求x,y的最大公約數(shù)z的程序，即z=gcd(x,y)。STARTRead(x,y)x<>0y>=xy:=y-xxyz:=ySTOPTFTFI(x,y)aP(x,y)bcO(x,y,z)deg······不變式斷言法輸入斷言：例：設(shè)x,y為非負(fù)整數(shù)，求x,y的最大91子目標(biāo)斷言法(建立斷言)輸入斷言

I(x,y):x0>=0∧

y0>=0∧(x0≠0∨y0≠0)輸出斷言O(shè)(x,y,z):z=gcd(x,y)子目標(biāo)斷言P(x,y,yend):x>=0∧y>=0∧(x≠0∨y≠0)

=>yend=gcd(x,y)STARTRead(x,y)x<>0y>=xy:=y-xxyz:=ySTOPTFTFI(x,y)aP(x,y,yend)bcO(x,y,z)deg······子目標(biāo)斷言法(建立斷言)輸入斷言STARTRe92子目標(biāo)斷言法(建立檢驗條件)通路1： 控制轉(zhuǎn)出循環(huán)時，子目標(biāo)斷言成立。通路2、通路3： 如果在通過循環(huán)之后，子目標(biāo)斷言在斷點處成立，那么，在通過循環(huán)之前，斷言也成立。通路4： 如果輸入斷言為真，且控制第一次通過斷點B時子目標(biāo)斷言為真，則輸出斷言為真。子目標(biāo)斷言法(建立檢驗條件)通路1：93子目標(biāo)斷言法(建立檢驗條件)通路1：b->c檢驗條件1

x=0=>P(x,y,yend)x=0=>

[x>=0∧y>=0∧

(x≠0∨y≠0)

=> yend=gcd(x,y)]

通路2：b->d->b檢驗條件2P(x,y-x,yend)∧x<>0∧y>=x=>P(x,y,yend)[x>=0∧y-x>=0∧

(x≠0∨y-x≠0)

=>yend=gcd(x,y-x)]∧x<>0∧y>=x=>

[x>=0∧y>=0∧(x≠0∨y≠0)

=>yend=gcd(x,y)]通路3：b->e->b檢驗條件3P(y,x,yend)∧x<>0∧y<x=>P(x,y,yend)通路4：a->b檢驗條件4x0>=0∧

y0>=0∧

(x0

≠0∨y0

≠0)

∧P(x0,y0,yend)=>yend=gcd(x0,y0)子目標(biāo)斷言法(建立檢驗條件)通路1：b->c94子目標(biāo)斷言法(證明檢驗條件)檢驗條件1： x=0=>[x>=0∧y>=0=>yend=gcd(x,y)]證明： 因為有x=0,yend=y 所以yend=y=gcd(0,y)=gcd(x,y)檢驗條件2：P(x,y-x,yend)∧x<>0∧y>x=>P(x,y,yend)即證明：[

x>=0∧y-x>=0∧(x≠0∨y-x≠0)=>

yend=gcd(x,y-x)]∧x<>0∧y>=x=>

[x>=0∧y>=0∧(x≠0∨y≠0)=>

yend=gcd(x,y)]

子目標(biāo)斷言法(證明檢驗條件)檢驗條件1：95程序部分正確但不終止實例例：求兩個非負(fù)整數(shù)x、y的最大公約數(shù)z的程序。ProgramAvarx,y,z,s:integer;beginread(x,y);whilex≠0doify>xtheny=y–x;elsex=x–y;z=y;write(z);end.STARTRead(x,y)x≠0y>xy:=y-xx:=x-yz:=ySTOPTFTFI(x,y)aP(x,y)bcO(x,y,z)deg······可以利用不變式斷言等方法證明該程序的部分正確性，但無法證明它是終止的。因為當(dāng)y＝0時，程序循環(huán)將不終止！

程序部分正確但不終止實例例：求兩個非負(fù)整數(shù)x、y的最大公約數(shù)96第5章程序正確性證明5.1程序正確性驗證概述5.2不變式斷言法5.3子目標(biāo)斷言法5.4界函數(shù)法－－計數(shù)器法第5章程序正確性證明5.1程序正確性驗證概述975.4計數(shù)器方法證明程序終止性證明思路 通過估計循環(huán)執(zhí)行的最大次數(shù)證明程序終止性的方法。證明步驟:1.為程序的每一個循環(huán)附加一個新的變量作為該循環(huán)的計數(shù)器，初始值置為0，每循環(huán)一次該計數(shù)器加1。2.為每個循環(huán)設(shè)置一個中間斷言，它表示相應(yīng)的計數(shù)器不會超過固定的界限。3.證明（2）中的中間斷言是不變式斷言。5.4計數(shù)器方法證明程序終止性證明思路98計數(shù)器方法證明程序終止性實例計算非負(fù)整數(shù)的最大公約數(shù)varx,y,z,s:integer;beginRead(x,y)whilex≠0dobeginIfy≥xthen y:=y-x;else s:=x;x:=y;y:=s;endz:=y;write(z);endSTARTRead(x,y)x≠0y≥xy:=y-xxyz:=ySTOPTFTFI(x,y)aP(x,y)bO(x,y)de····c·計數(shù)器方法證明程序終止性實例計算非負(fù)整數(shù)的最大公約數(shù)var99計數(shù)器方法證明程序終止性實例1.引進(jìn)計數(shù)器I,并建立如下斷言

x≥0∧y≥0∧2x+y+I≤2x0+y0

varx,y,z,s:integer;