2013教科版選修1《程序設(shè)計(jì)的基本方法》課件2

第三課

程序設(shè)計(jì)方法學(xué)基本理論

——程序正確性證明第三課

程序設(shè)計(jì)方法學(xué)基本理論

——程序正確性證1什么樣的程序才是正確的？如何來(lái)保證程序是正確的？程序正確性概述什么樣的程序才是正確的？如何來(lái)保證程序是正確的？程序正確2關(guān)于程序正確性的認(rèn)識(shí)根據(jù)問(wèn)題的特性和軟件所要實(shí)現(xiàn)的功能，選擇一些具有代表性的數(shù)據(jù)，設(shè)計(jì)測(cè)試用例。通過(guò)用例程序執(zhí)行，去發(fā)現(xiàn)被測(cè)試程序的錯(cuò)誤。什么樣的程序才是正確的？

“測(cè)試”或“調(diào)試”方法采用“測(cè)試”方法可以發(fā)現(xiàn)程序中的錯(cuò)誤，但卻不能證明程序中沒(méi)有錯(cuò)誤！

因此，為保證程序的正確性，必須從理論上研究有關(guān)“程序正確性證明”的方法。關(guān)于程序正確性的認(rèn)識(shí)根據(jù)問(wèn)題的特性和軟件所要3程序正確性證明發(fā)展歷程20世紀(jì)50年代Turing開(kāi)始研究1967年，F(xiàn)loyd和Naur提出不變式斷言法1969年，Hoare提出公理化方法1975年，Dijkstra提出最弱前置謂詞和程序推導(dǎo)方法，解決了斷言構(gòu)造難的問(wèn)題，可從程序規(guī)約推導(dǎo)出正確程序，使正確性證明變得實(shí)用。程序正確性理論是十分活躍的課題，不僅可以證明順序程序的正確性，而且還可以證明非確定性程序，以及并行程序的正確性。程序正確性證明發(fā)展歷程20世紀(jì)50年代Turing開(kāi)始研究4程序正確性理論程序設(shè)計(jì)的一般過(guò)程程序正確性理論程序設(shè)計(jì)的一般過(guò)程5程序正確性理論程序功能的精確描述1、程序規(guī)約：對(duì)程序所實(shí)現(xiàn)功能的精確描述，由程序的前置斷言和后置斷言兩部分組成。2、前置斷言：程序執(zhí)行前的輸入應(yīng)滿足的條件，又稱為輸入斷言。3、后置斷言：程序執(zhí)行后的輸出應(yīng)滿足的條件，又稱為輸出斷言。程序設(shè)計(jì)過(guò)程：?jiǎn)栴}程序規(guī)約程序程序正確性理論程序功能的精確描述1、程序規(guī)約：對(duì)6程序規(guī)約的基本分類非形式化程序規(guī)約非形式化程序規(guī)約采用自然語(yǔ)言描述程序功能，簡(jiǎn)單、方便，但存在二義性，因此，不利于程序的正確性證明。形式化程序規(guī)約采用數(shù)學(xué)化的語(yǔ)言描述程序功能，描述精確，無(wú)二義性，便于程序的正確性證明。程序規(guī)約的基本分類非形式化程序規(guī)約7程序規(guī)約的實(shí)例（1/2）在書(shū)寫(xiě)程序規(guī)約時(shí)，使用Q表示前置斷言，R表示后置斷言，S表示問(wèn)題求解的實(shí)現(xiàn)程序。在前置斷言Q之前，還必須給出Q和R中所出現(xiàn)的標(biāo)識(shí)符的必要說(shuō)明。例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í)例（1/2）在書(shū)寫(xiě)程序規(guī)約時(shí)，使用Q表示前置斷言8例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):i)}程序規(guī)約的實(shí)例（2/2）例2：求兩個(gè)非負(fù)整數(shù)的最大公約數(shù)。程序規(guī)約的實(shí)例（2/2）9程序正確性定義（1/3）衡量一個(gè)程序的正確性，主要看程序是否實(shí)現(xiàn)了問(wèn)題所要求的功能。若程序?qū)崿F(xiàn)了問(wèn)題所要求的功能，則稱它為正確的，否則是不正確的。

程序設(shè)計(jì)過(guò)程：?jiǎn)栴}程序規(guī)約程序

對(duì)程序的正確性理解，可以分為兩個(gè)層次：從廣義來(lái)說(shuō)，一個(gè)程序的正確性取決于該程序滿足問(wèn)題實(shí)際需求的程度。從狹義而言，如果一個(gè)程序滿足了它的程序規(guī)約就是正確的。

程序正確性定義（1/3）衡量一個(gè)程序的正確性，主要看程序是否10程序規(guī)約Q{S}R是一個(gè)邏輯表達(dá)式，其取值為真或假，其中取值為真的含義是指：給定一段程序S，若程序開(kāi)始執(zhí)行之前Q為真，S的執(zhí)行將終止，且終止時(shí)R為真，則稱為“程序S，關(guān)于前置斷言Q和后置斷言R是完全正確的”。程序正確性定義（2/3）程序規(guī)約Q{S}R是一個(gè)邏輯表達(dá)式，其取值為真或假，其中11部分正確：若對(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)為真，并且程序S的計(jì)算都將終止的輸入信息i，R(i,S(i))都為真，則稱程序S關(guān)于Q和R是完全正確的。一個(gè)程序的完全正確，等價(jià)于該程序是部分正確，同時(shí)又是終止的。程序正確性定義（3/3）部分正確：若對(duì)于每個(gè)使得Q(i)為真，并且程序S計(jì)算終止的輸12（1）證明部分正確性的方法

A.Floyd的不變式斷言法

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

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

A.Floyd的良序集方法

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

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

A.Hoare公理化方法的推廣

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

C.Dijkstra的弱謂詞變換方法以及強(qiáng)驗(yàn)證方法程序正確性的證明方法分類（1）證明部分正確性的方法程序正確性的證明方法分類13循環(huán)不變式斷言把反映循環(huán)變量的變化規(guī)律，且在每次循環(huán)體的執(zhí)行前后均為真的邏輯表達(dá)式稱為該循環(huán)的不變式斷言。例帶余整數(shù)除法問(wèn)題：設(shè)x為非負(fù)整數(shù)，y為正整數(shù)，求x除以y的商q，以及余數(shù)r。

程序：q＝0；r＝x；while(r≥y)//該循環(huán)不變式斷言：{//(x＝y(tǒng)×q＋r)∧r≥0r＝r－y；q＝q＋1；}循環(huán)不變式斷言把反映循環(huán)變量的變化規(guī)律，且在每次循環(huán)體的執(zhí)行14不變式斷言法證明步驟：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)椴糠终_的。不變式斷言法15不變式斷言法實(shí)例例：設(shè)x,y為正整數(shù)，求x,y的最大公約數(shù)z的程序，即z=gcd(x,y)。Functiongcd(x1,x2:integer); vary1,y2,z:Integer;Begin y1:=x1;y2:=x1; whiley1<>y2do ify1>y2theny1:=y1-y2elsey2:=y2-y1end;z:=y1;write(z);End.START(x1,x2)->(y1,y2)y1<>y2y1>y2y1:=y1-y2y2:=y2-y1z:=y1STOPTFTF不變式斷言法實(shí)例例：設(shè)x,y為正整數(shù)，求x,y的最大公約數(shù)z16不變式斷言法實(shí)例(建立斷言)輸入斷言：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)START(x1,x2)->(y1,y2)y1<>y2y1>y2y1:=y1-y2y2:=y2-y1z:=y1STOPTFTFI(x1,x2)aP(x1,x2,y1,y2)bcO(x,y,z)deg

通路劃分：通路1：a->b通路2：b->d->b通路3：b->e->b通路4：b->g->c···不變式斷言法實(shí)例(建立斷言)輸入斷言：START(x1,x217不變式斷言法實(shí)例(建立檢驗(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)通路3：P(x1,x2,y1,y2)^y1<>y2^y1<y2=>P(x1,x2,y1,y2-y1)通路4：P(x1,x2,y1,y2)^y1=y2=>O(x1,x2,z)

不變式斷言法實(shí)例(建立檢驗(yàn)條件)檢驗(yàn)條件：I^R=18不變式斷言法實(shí)例(證明檢驗(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=z

P(x1,x2,y1,y2)^y1=y2=>O(x1,x2,z)不變式斷言法實(shí)例(證明檢驗(yàn)條件)通路1：19不變式斷言法實(shí)例對(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開(kāi)始(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)TF···不變式斷言法實(shí)例對(duì)任一給定的自然數(shù)x，計(jì)算z＝[]20不變式斷言法實(shí)例檢驗(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+1=2(y1+1)+1通路3：B->CP(x,y1,y2,y3)^y2>x=>O(x,y)y12<x^y2=(y1+1)2^y3=2y1+1^y2>x=>y12<x<(y1+1)2不變式斷言法實(shí)例檢驗(yàn)條件：I^R=O21不變式斷言法實(shí)例檢驗(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+1=2(y1+1)+1證明：

x≥(y1+1)2y2+y3+2=(y1+1)2+2y1+1+2=(y1+2)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í)例檢驗(yàn)條件222子目標(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)行歸納。子目標(biāo)斷言法子目標(biāo)斷言法與不變式斷言法的主要區(qū)別是：23不變式斷言法輸入斷言：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)STARTRead(x,y)x<>0y>=xy:=y-xxyz:=ySTOPTFTFI(x,y)aP(x,y)bcO(x,y,z)deg例：設(shè)x,y為正整數(shù)，求x,y的最大公約數(shù)z的程序，即z=gcd(x,y)。不變式斷言法輸入斷言：STARTRead(x,y)x<>0y24子目標(biāo)斷言法(建立斷言)輸入斷言I(x,y):x0>=0^y0>=0輸出斷言O(shè)(x,y,z):z=gcd(x,y)子目標(biāo)斷言P(x,y,yend):x>=0^y>=0

=>yend=gcd(x,y)STARTRead(x,y)x<>0y>=xy:=y-xxyz:=ySTOPTFTFI(x,y)aP(x,y)bcO(x,y,z)deg子目標(biāo)斷言法(建立斷言)輸入斷言STARTRead(x,y)25子目標(biāo)斷言法(建立檢驗(yàn)條件)通路1：b->c檢驗(yàn)條件1x=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^yend=gcd(x,y-x)^x<>0^y>x=>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^P(x0,y0,yend)=>yend=gcd(x0,y0)子目標(biāo)斷言法(建立檢驗(yàn)條件)通路1：b->c26子目標(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^yend=gcd(x,y-x)^x<>0^y>x=>x>=0^y>=0^yend=gcd(x,y)由：x<>0^y>x=>y>0,以及gcd(x,y-x)=gcd(x,y)，當(dāng)且僅當(dāng)x>0,y>0可知yend＝gcd(x,y-x)＝gcd(x,y)子目標(biāo)斷言法(證明檢驗(yàn)條件)檢驗(yàn)條件1：27第三課

程序設(shè)計(jì)方法學(xué)基本理論

——程序正確性證明第三課

程序設(shè)計(jì)方法學(xué)基本理論

——程序正確性證28什么樣的程序才是正確的？如何來(lái)保證程序是正確的？程序正確性概述什么樣的程序才是正確的？如何來(lái)保證程序是正確的？程序正確29關(guān)于程序正確性的認(rèn)識(shí)根據(jù)問(wèn)題的特性和軟件所要實(shí)現(xiàn)的功能，選擇一些具有代表性的數(shù)據(jù)，設(shè)計(jì)測(cè)試用例。通過(guò)用例程序執(zhí)行，去發(fā)現(xiàn)被測(cè)試程序的錯(cuò)誤。什么樣的程序才是正確的？

“測(cè)試”或“調(diào)試”方法采用“測(cè)試”方法可以發(fā)現(xiàn)程序中的錯(cuò)誤，但卻不能證明程序中沒(méi)有錯(cuò)誤！

因此，為保證程序的正確性，必須從理論上研究有關(guān)“程序正確性證明”的方法。關(guān)于程序正確性的認(rèn)識(shí)根據(jù)問(wèn)題的特性和軟件所要30程序正確性證明發(fā)展歷程20世紀(jì)50年代Turing開(kāi)始研究1967年，F(xiàn)loyd和Naur提出不變式斷言法1969年，Hoare提出公理化方法1975年，Dijkstra提出最弱前置謂詞和程序推導(dǎo)方法，解決了斷言構(gòu)造難的問(wèn)題，可從程序規(guī)約推導(dǎo)出正確程序，使正確性證明變得實(shí)用。程序正確性理論是十分活躍的課題，不僅可以證明順序程序的正確性，而且還可以證明非確定性程序，以及并行程序的正確性。程序正確性證明發(fā)展歷程20世紀(jì)50年代Turing開(kāi)始研究31程序正確性理論程序設(shè)計(jì)的一般過(guò)程程序正確性理論程序設(shè)計(jì)的一般過(guò)程32程序正確性理論程序功能的精確描述1、程序規(guī)約：對(duì)程序所實(shí)現(xiàn)功能的精確描述，由程序的前置斷言和后置斷言兩部分組成。2、前置斷言：程序執(zhí)行前的輸入應(yīng)滿足的條件，又稱為輸入斷言。3、后置斷言：程序執(zhí)行后的輸出應(yīng)滿足的條件，又稱為輸出斷言。程序設(shè)計(jì)過(guò)程：?jiǎn)栴}程序規(guī)約程序程序正確性理論程序功能的精確描述1、程序規(guī)約：對(duì)33程序規(guī)約的基本分類非形式化程序規(guī)約非形式化程序規(guī)約采用自然語(yǔ)言描述程序功能，簡(jiǎn)單、方便，但存在二義性，因此，不利于程序的正確性證明。形式化程序規(guī)約采用數(shù)學(xué)化的語(yǔ)言描述程序功能，描述精確，無(wú)二義性，便于程序的正確性證明。程序規(guī)約的基本分類非形式化程序規(guī)約34程序規(guī)約的實(shí)例（1/2）在書(shū)寫(xiě)程序規(guī)約時(shí)，使用Q表示前置斷言，R表示后置斷言，S表示問(wèn)題求解的實(shí)現(xiàn)程序。在前置斷言Q之前，還必須給出Q和R中所出現(xiàn)的標(biāo)識(shí)符的必要說(shuō)明。例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í)例（1/2）在書(shū)寫(xiě)程序規(guī)約時(shí)，使用Q表示前置斷言35例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):i)}程序規(guī)約的實(shí)例（2/2）例2：求兩個(gè)非負(fù)整數(shù)的最大公約數(shù)。程序規(guī)約的實(shí)例（2/2）36程序正確性定義（1/3）衡量一個(gè)程序的正確性，主要看程序是否實(shí)現(xiàn)了問(wèn)題所要求的功能。若程序?qū)崿F(xiàn)了問(wèn)題所要求的功能，則稱它為正確的，否則是不正確的。

程序設(shè)計(jì)過(guò)程：?jiǎn)栴}程序規(guī)約程序

對(duì)程序的正確性理解，可以分為兩個(gè)層次：從廣義來(lái)說(shuō)，一個(gè)程序的正確性取決于該程序滿足問(wèn)題實(shí)際需求的程度。從狹義而言，如果一個(gè)程序滿足了它的程序規(guī)約就是正確的。

程序正確性定義（1/3）衡量一個(gè)程序的正確性，主要看程序是否37程序規(guī)約Q{S}R是一個(gè)邏輯表達(dá)式，其取值為真或假，其中取值為真的含義是指：給定一段程序S，若程序開(kāi)始執(zhí)行之前Q為真，S的執(zhí)行將終止，且終止時(shí)R為真，則稱為“程序S，關(guān)于前置斷言Q和后置斷言R是完全正確的”。程序正確性定義（2/3）程序規(guī)約Q{S}R是一個(gè)邏輯表達(dá)式，其取值為真或假，其中38部分正確：若對(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)為真，并且程序S的計(jì)算都將終止的輸入信息i，R(i,S(i))都為真，則稱程序S關(guān)于Q和R是完全正確的。一個(gè)程序的完全正確，等價(jià)于該程序是部分正確，同時(shí)又是終止的。程序正確性定義（3/3）部分正確：若對(duì)于每個(gè)使得Q(i)為真，并且程序S計(jì)算終止的輸39（1）證明部分正確性的方法

A.Floyd的不變式斷言法

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

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

A.Floyd的良序集方法

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

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

A.Hoare公理化方法的推廣

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

C.Dijkstra的弱謂詞變換方法以及強(qiáng)驗(yàn)證方法程序正確性的證明方法分類（1）證明部分正確性的方法程序正確性的證明方法分類40循環(huán)不變式斷言把反映循環(huán)變量的變化規(guī)律，且在每次循環(huán)體的執(zhí)行前后均為真的邏輯表達(dá)式稱為該循環(huán)的不變式斷言。例帶余整數(shù)除法問(wèn)題：設(shè)x為非負(fù)整數(shù)，y為正整數(shù)，求x除以y的商q，以及余數(shù)r。

程序：q＝0；r＝x；while(r≥y)//該循環(huán)不變式斷言：{//(x＝y(tǒng)×q＋r)∧r≥0r＝r－y；q＝q＋1；}循環(huán)不變式斷言把反映循環(huán)變量的變化規(guī)律，且在每次循環(huán)體的執(zhí)行41不變式斷言法證明步驟：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)椴糠终_的。不變式斷言法42不變式斷言法實(shí)例例：設(shè)x,y為正整數(shù)，求x,y的最大公約數(shù)z的程序，即z=gcd(x,y)。Functiongcd(x1,x2:integer); vary1,y2,z:Integer;Begin y1:=x1;y2:=x1; whiley1<>y2do ify1>y2theny1:=y1-y2elsey2:=y2-y1end;z:=y1;write(z);End.START(x1,x2)->(y1,y2)y1<>y2y1>y2y1:=y1-y2y2:=y2-y1z:=y1STOPTFTF不變式斷言法實(shí)例例：設(shè)x,y為正整數(shù)，求x,y的最大公約數(shù)z43不變式斷言法實(shí)例(建立斷言)輸入斷言：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)START(x1,x2)->(y1,y2)y1<>y2y1>y2y1:=y1-y2y2:=y2-y1z:=y1STOPTFTFI(x1,x2)aP(x1,x2,y1,y2)bcO(x,y,z)deg

通路劃分：通路1：a->b通路2：b->d->b通路3：b->e->b通路4：b->g->c···不變式斷言法實(shí)例(建立斷言)輸入斷言：START(x1,x244不變式斷言法實(shí)例(建立檢驗(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)通路3：P(x1,x2,y1,y2)^y1<>y2^y1<y2=>P(x1,x2,y1,y2-y1)通路4：P(x1,x2,y1,y2)^y1=y2=>O(x1,x2,z)

不變式斷言法實(shí)例(建立檢驗(yàn)條件)檢驗(yàn)條件：I^R=45不變式斷言法實(shí)例(證明檢驗(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=z

P(x1,x2,y1,y2)^y1=y2=>O(x1,x2,z)不變式斷言法實(shí)例(證明檢驗(yàn)條件)通路1：46不變式斷言法實(shí)例對(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開(kāi)始(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)TF···不變式斷言法實(shí)例對(duì)任一給定的自然數(shù)x，計(jì)算z＝[]47不變式斷言法實(shí)例檢驗(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+1=2(y1+1)+1通路3：B->CP(x,y1,y2,y3)^y2>x=>O(x,y)y12<x^y2=(y1+1)2^y3=2y1+1^y2>x=>y12<x<(y1+1)2不變式斷言法實(shí)例檢驗(yàn)條件：I^R=O48不變式斷言法實(shí)例檢驗(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+1=2(y1+1)+1證明：

x≥(y1+1)2y2+y3+2=(y1+1)2+2y1+1+2=(y1+2)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í)例檢驗(yàn)條件249子目標(biāo)斷言法子目標(biāo)斷言法與不變式斷言法的主要區(qū)別是：兩種方法對(duì)循環(huán)所建立的斷言不同。不變式斷言描述了程序變量y的中間值與初始值之間關(guān)系，而子目標(biāo)斷言法描述的是y的中間值與循環(huán)終止時(shí)的最終值yend之間的關(guān)系。兩種方法進(jìn)行歸納的方向不同。不變式斷言沿著程