程序正確性證明概述課件

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

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

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

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

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

A.Floyd的不變式斷言法

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

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

A.Floyd的良序集方法

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

C.Manna等人的不動(dòng)點(diǎn)方法完全正確性的方法

A.Hoare公理化方法的推廣

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

C.Dijkstra的弱謂詞變換方法以及強(qiáng)驗(yàn)證方法程序正確性的證明方法分類證明部分正確性的方法21第5章程序正確性證明5.1程序正確性驗(yàn)證概述5.2不變式斷言法5.3子目標(biāo)斷言法5.4界函數(shù)法－－計(jì)數(shù)器法第5章程序正確性證明5.1程序正確性驗(yàn)證概述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)中選取一個(gè)斷點(diǎn)，在斷點(diǎn)處建立一個(gè)循環(huán)不變式斷言。2、建立檢驗(yàn)條件 將程序分解為不同的通路，為每一個(gè)通路建立一個(gè)檢驗(yàn)條件，該檢驗(yàn)條件為如下形式：

I∧R=>O

其中I為輸入斷言，R為進(jìn)入通路的條件，O為輸出斷言。3、證明檢驗(yàn)條件 運(yùn)用數(shù)學(xué)工具證明步驟2得到的所有檢驗(yàn)條件，如果每一條通路檢驗(yàn)條件都為真，則該程序?yàn)椴糠终_的。5.2不變式斷言法證明步驟：24不變式斷言法實(shí)例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不變式斷言法實(shí)例1例：設(shè)x,y為正整數(shù)，求x,y的最大公約數(shù)25不變式斷言法實(shí)例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······不變式斷言法實(shí)例1(建立斷言)輸入斷言：通路劃分：ST26不變式斷言法實(shí)例1(建立檢驗(yàn)條件)檢驗(yàn)條件：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)不變式斷言法實(shí)例1(建立檢驗(yàn)條件)檢驗(yàn)條件：I∧R=27不變式斷言法實(shí)例1(建立檢驗(yàn)條件)通路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)不變式斷言法實(shí)例1(建立檢驗(yàn)條件)通路3：28不變式斷言法實(shí)例1(證明檢驗(yàn)條件)通路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)不變式斷言法實(shí)例1(證明檢驗(yàn)條件)通路1：29不變式斷言法實(shí)例2對(duì)任一給定的自然數(shù)x，計(jì)算z＝[]，即計(jì)算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····不變式斷言法實(shí)例2對(duì)任一給定的自然數(shù)x，計(jì)算z＝[30不變式斷言法實(shí)例2檢驗(yàn)條件：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不變式斷言法實(shí)例2檢驗(yàn)條件：I∧R=>O31不變式斷言法實(shí)例2檢驗(yàn)條件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檢驗(yàn)條件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不變式斷言法實(shí)例2檢驗(yàn)條件232作業(yè)課本P174習(xí)題1、習(xí)題2。要求用不變式斷言法證明。作業(yè)課本P174習(xí)題1、習(xí)題2。要求用不變式斷言法證明。33第5章程序正確性證明5.1程序正確性驗(yàn)證概述5.2不變式斷言法5.3子目標(biāo)斷言法5.4界函數(shù)法－－計(jì)數(shù)器法第5章程序正確性證明5.1程序正確性驗(yàn)證概述345.3子目標(biāo)斷言法子目標(biāo)斷言法與不變式斷言法的主要區(qū)別是：兩種方法對(duì)循環(huán)所建立的斷言不同。不變式斷言描述了程序變量y的中間值與初始值之間關(guān)系；子目標(biāo)斷言法描述的是y的中間值與循環(huán)終止時(shí)的最終值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)斷言法(建立檢驗(yàn)條件)通路1： 控制轉(zhuǎn)出循環(huán)時(shí)，子目標(biāo)斷言成立。通路2、通路3： 如果在通過循環(huán)之后，子目標(biāo)斷言在斷點(diǎn)處成立，那么，在通過循環(huán)之前，斷言也成立。通路4： 如果輸入斷言為真，且控制第一次通過斷點(diǎn)B時(shí)子目標(biāo)斷言為真，則輸出斷言為真。子目標(biāo)斷言法(建立檢驗(yàn)條件)通路1：38子目標(biāo)斷言法(建立檢驗(yàn)條件)通路1：b->c檢驗(yàn)條件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檢驗(yàn)條件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檢驗(yàn)條件3P(y,x,yend)∧x<>0∧y<x=>P(x,y,yend)通路4：a->b檢驗(yàn)條件4x0>=0∧

y0>=0∧

(x0

≠0∨y0

≠0)

∧P(x0,y0,yend)=>yend=gcd(x0,y0)子目標(biāo)斷言法(建立檢驗(yàn)條件)通路1：b->c39子目標(biāo)斷言法(證明檢驗(yàn)條件)檢驗(yàn)條件1： x=0=>[x>=0∧y>=0=>yend=gcd(x,y)]證明： 因?yàn)橛衳=0,yend=y 所以yend=y=gcd(0,y)=gcd(x,y)檢驗(yàn)條件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)斷言法(證明檢驗(yàn)條件)檢驗(yàn)條件1：40程序部分正確但不終止實(shí)例例：求兩個(gè)非負(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······可以利用不變式斷言等方法證明該程序的部分正確性，但無法證明它是終止的。因?yàn)楫?dāng)y＝0時(shí)，程序循環(huán)將不終止！

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

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

varx,y,z,s:integer;read(x,y);I:=0;//計(jì)數(shù)器賦初值whilex≠0dobeginify≥xtheny:=y-x; elses:=x;x:=y;y:=sfi;I:=I+1;//計(jì)數(shù)器遞增End;z:=y;write(z);計(jì)數(shù)器方法證明程序終止性實(shí)例1.引進(jìn)計(jì)數(shù)器I,并建立如下斷言45計(jì)數(shù)器方法證明程序終止性實(shí)例2.建立檢驗(yàn)條件并證明，從而證明計(jì)數(shù)器斷言為不變式斷言。檢驗(yàn)條件1：a->b [x0≥0∧y0≥0]=>[x0≥0∧y0≥0∧2x0+y0+0≤2x0+y0]檢驗(yàn)條件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檢驗(yàn)條件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í)行有限次，即程序終止。采用計(jì)數(shù)器方法證明程序終止性和利用不變式斷言法證明部分正確性步驟完全類似，只要再添加輸出斷言部分檢驗(yàn)條件并證明，即可完成程序部分正確性證明。因此，可以把上述兩者聯(lián)合起來，完成程序的完全正確性證明。

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

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

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

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

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

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

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

A.Floyd的不變式斷言法

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

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

A.Floyd的良序集方法

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

C.Manna等人的不動(dòng)點(diǎn)方法完全正確性的方法

A.Hoare公理化方法的推廣

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

C.Dijkstra的弱謂詞變換方法以及強(qiáng)驗(yàn)證方法程序正確性的證明方法分類證明部分正確性的方法76第5章程序正確性證明5.1程序正確性驗(yàn)證概述5.2不變式斷言法5.3子目標(biāo)斷言法5.4界函數(shù)法－－計(jì)數(shù)器法第5章程序正確性證明5.1程序正確性驗(yàn)證概述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)中選取一個(gè)斷點(diǎn)，在斷點(diǎn)處建立一個(gè)循環(huán)不變式斷言。2、建立檢驗(yàn)條件 將程序分解為不同的通路，為每一個(gè)通路建立一個(gè)檢驗(yàn)條件，該檢驗(yàn)條件為如下形式：

I∧R=>O

其中I為輸入斷言，R為進(jìn)入通路的條件，O為輸出斷言。3、證明檢驗(yàn)條件 運(yùn)用數(shù)學(xué)工具證明步驟2得到的所有檢驗(yàn)條件，如果每一條通路檢驗(yàn)條件都為真，則該程序?yàn)椴糠终_的。5.2不變式斷言法證明步驟：79不變式斷言法實(shí)例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不變式斷言法實(shí)例1例：設(shè)x,y為正整數(shù)，求x,y的最大公約數(shù)80不變式斷言法實(shí)例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······不變式斷言法實(shí)例1(建立斷言)輸入斷言：通路劃分：ST81不變式斷言法實(shí)例1(建立檢驗(yàn)條件)檢驗(yàn)條件：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)不變式斷言法實(shí)例1(建立檢驗(yàn)條件)檢驗(yàn)條件：I∧R=82不變式斷言法實(shí)例1(建立檢驗(yàn)條件)通路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)不變式斷言法實(shí)例1(建立檢驗(yàn)條件)通路3：83不變式斷言法實(shí)例1(證明檢驗(yàn)條件)通路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)不變式斷言法實(shí)例1(證明檢驗(yàn)條件)通路1：84不變式斷言法實(shí)例2對(duì)任一給定的自然數(shù)x，計(jì)算z＝[]，即計(jì)算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····不變式斷言法實(shí)例2對(duì)任一給定的自然數(shù)x，計(jì)算z＝[85不變式斷言法實(shí)例2檢驗(yàn)條件：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不變式斷言法實(shí)例2檢驗(yàn)條件：I∧R=>O86不變式斷言法實(shí)例2檢驗(yàn)條件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檢驗(yàn)條件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不變式斷言法實(shí)例2檢驗(yàn)條件287作業(yè)課本P174習(xí)題1、習(xí)題2。要求用不變式斷言法證明。作業(yè)課本P174習(xí)題1、習(xí)題2。要求用不變式斷言法證明。88第5章程序正確性證明5.1程序正確性驗(yàn)證概述5.2不變式斷言法5.3子目標(biāo)斷言法5.4界函數(shù)法－－計(jì)數(shù)器法第5章程序正確性證明5.1程序正確性驗(yàn)證概述895.3子目標(biāo)斷言法子目標(biāo)斷言法與不變式斷言法的主要區(qū)別是：兩種方法對(duì)循環(huán)所建立的斷言不同。不變式斷言描述了程序變量y的中間值與初始值之間關(guān)系；子目標(biāo)斷言法描述的是y的中間值與循環(huán)終止時(shí)的最終值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)斷言法(建立檢驗(yàn)條件)通路1： 控制轉(zhuǎn)出循環(huán)時(shí)，子目標(biāo)斷言成立。通路2、通路3： 如果在通過循環(huán)之后，子目標(biāo)斷言在斷點(diǎn)處成立，那么，在通過循環(huán)之前，斷言也成立。通路4： 如果輸入斷言為真，且控制第一次通過斷點(diǎn)B時(shí)子目標(biāo)斷言為真，則輸出斷言為真。子目標(biāo)斷言法(建立檢驗(yàn)條件)通路1：93子目標(biāo)斷言法(建立檢驗(yàn)條件)通路1：b->c檢驗(yàn)條件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檢驗(yàn)條件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檢驗(yàn)條件3P(y,x,yend)∧x<>0∧y<x=>P(x,y,yend)通路4：a->b檢驗(yàn)條件4x0>=0∧

y0>=0∧

(x0

≠0∨y0

≠0)

∧P(x0,y0,yend)=>yend=gcd(x0,y0)子目標(biāo)斷言法(建立檢驗(yàn)條件)通路1：b->c94子目標(biāo)斷言法(證明檢驗(yàn)條件)檢驗(yàn)條件1： x=0=>[x>=0∧y>=0=>yend=gcd(x,y)]證明： 因?yàn)橛衳=0,yend=y 所以yend=y=gcd(0,y)=gcd(x,y)檢驗(yàn)條件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)斷言法(證明檢驗(yàn)條件)檢驗(yàn)條件1：95程序部分正確但不終止實(shí)例例：求兩個(gè)非負(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······可以利用不變式斷言等方法證明該程序的部分正確性，但無法證明它是終止的。因?yàn)楫?dāng)y＝0時(shí)，程序循環(huán)將不終止！

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

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

varx,y,z,s:integer;