公理語義-Mann子目標(biāo)Hoare

程序設(shè)計(jì)形式語義學(xué)南京理工大學(xué)計(jì)算機(jī)系張琨二○○四年八月二日程序設(shè)計(jì)形式語義學(xué)2公理語義試圖通過在程序邏輯的范圍內(nèi)給出證明規(guī)則來確定程序設(shè)計(jì)構(gòu)造的含義。該方法的代表人物是R.W.Floyd和C.A.R.Hoare。從一開始，公理語義強(qiáng)調(diào)的是正確性證明。2.5程序正確性證明－Manna的子目標(biāo)斷言法美國斯坦福大學(xué)的Z.Manna教授在Floyd的不變式斷言法的基礎(chǔ)上，提出了部分正確性證明的子目標(biāo)法。子目標(biāo)法與不變式法的主要區(qū)別在于：在斷言設(shè)置中，不變式法的斷言描述程序處理過程中的中間變量與初始值之間的關(guān)系，而子目標(biāo)斷言中描述的是中間變量與終值間的關(guān)系其歸納推理方向不同。不變式斷言法沿程序執(zhí)行方向正向推理，而子目標(biāo)法沿程序執(zhí)行的反方向逆向歸納推理。2.5程序正確性證明－Manna的子目標(biāo)斷言法1.建立輸入、輸出和循環(huán)不變式斷言 設(shè)x，y的初始值為x0，y0，可分別建立輸入斷言I、輸出斷言O(shè)、子目標(biāo)斷言如下： I(x):x0≥0∧y0≥0∧(x0≠0∨y0≠0) O(x,z):z=gcd(x0,y0) 子目標(biāo)斷言q(x,y,yf):x≥0∧y≥0∧(x≠0∨y≠0)=>yf=gcd(x,y)q(x,y,yf)的含義是：每當(dāng)控制以x和y的容許值通過L時(shí)，x，y的當(dāng)前值的最大公約數(shù)將等于y的最終值。2.5程序正確性證明－Manna的子目標(biāo)斷言法2.建立驗(yàn)證條件（采用逆向方法）首先證明當(dāng)控制最后一次通過L時(shí)，即控制轉(zhuǎn)出循環(huán)時(shí)，子目標(biāo)斷言成立。為此，由x=0退出本循環(huán)，要證明驗(yàn)證條件1：C1(x,y):x=0=>q(x,y,yf) 即：x=0=>[x≥0∧y≥0∧(x≠0∨y≠0)=>yf=gcd(x,y)其次，證明如果再通過循環(huán)后，子目標(biāo)斷言再L處成立，那么，再通過循環(huán)之前，斷言也成立。為此，要證明下面兩個(gè)驗(yàn)證條件。由x≠0∧y<x可推出驗(yàn)證條件2，即：C2(x,y):x≠0∧y<x∧q(y,x,yf)=>q(x,y,yf)由x≠0∧y≥x可推出驗(yàn)證條件3，即：C3(x,y):x≠0∧y≥x∧q(x,y-x,yf)=>q(x,y,yf)最后，證明如果輸入斷言為真，且當(dāng)控制第一次通過L時(shí)子目標(biāo)斷言為真，則輸出斷言為真。當(dāng)?shù)谝淮蔚竭_(dá)L點(diǎn)時(shí)，可推出驗(yàn)證條件4，即：C4(x,y):x0≥0∧y0≥0∧(x0≠0∨y0≠0)∧q(x0,y0,yf)=>yf=gcd(x0,y0)2.5程序正確性證明－Manna的子目標(biāo)斷言法3.證明驗(yàn)證條件驗(yàn)證條件1：C1(x,y):x=0=>q(x,y,yf)q(0,yf,yf) 即：x=0=>[0≥0∧yf≥0∧(0≠0∨yf≠0)=>yf=gcd(0,yf)]。驗(yàn)證條件2：C2(x,y):x≠0∧y<x∧q(y,x,yf)=>q(x,y,yf)即：x≠0∧y<x∧[y≥0∧x≥0∧(y≠0∨x≠0)=>yf=gcd(y,x)]=>[x≥0∧y≥0∧(x≠0∨y≠0)=>yf=gcd(x,y)]驗(yàn)證條件3，C3(x,y):x≠0∧y≥x∧q(x,y-x,yf)=>q(x,y,yf)即：x≠0∧y≥x∧[x≥0∧y-x≥0∧(x≠0∨y-x≠0)=>yf=gcd(x,y-x)]=>[x≥0∧y≥0∧(x≠0∨y≠0)=>yf=gcd(x,y)]驗(yàn)證條件4，C4(x,y):x0≥0∧y0≥0∧(x0≠0∨y0≠0)∧q(x0,y0,yf)=>yf=gcd(x0,y0)]2.5程序正確性證明－Hoare的公理化方法1969年，Hoare在Floyd的不變式斷言法基礎(chǔ)上，提出了一種證明程序部分正確性的Hoare公理化方法。根據(jù)結(jié)構(gòu)化定理，他提出了順序語句、條件語句、WHILE循環(huán)語句三種基本語句證明規(guī)則，試圖建立一個(gè)不變式演繹系統(tǒng)，以達(dá)到程序證明自動(dòng)化之目的。2.5程序正確性證明－Hoare的公理化方法定義2.8不變式語句

稱{P}S{Q}是不變式語句。其含義是：如果執(zhí)行S之前P為真，并且S執(zhí)行終止，Q為真，稱不變式語句為真或稱歸納表達(dá)式為真。Hoare公理系統(tǒng)的推理規(guī)則一般形式為：其中：B為不變式語句，是邏輯表達(dá)式或其他不變式語句，其含義是：為了推論B為真，只需證明前提Ai(i=1,2,…,n)為真。為了證明程序P關(guān)于輸入條件I(x)與輸出條件O(x,p(x))是部分正確的，歸結(jié)為證明不變式語句{I(x)}P{O(x,P(x))}為真。2.5程序正確性證明－Hoare的公理化方法Hoare提出的公理和相應(yīng)控制語句的證明規(guī)則。1.賦值語句公理設(shè)有賦值語句y←f(x)，則其公理為：{P(x,f(x,y))}y←f(x){P(x,y)}2.5程序正確性證明－Hoare的公理化方法Hoare提出的公理和相應(yīng)控制語句的證明規(guī)則。2.條件語句規(guī)則 {P∧R}S1{Q},{P∧﹁R}S2{Q} {P}IFRTHENS1ELSES2{Q} 或 {P∧R}S{Q},{P∧﹁R}=>{Q} {P}IFRTHENS{Q}2.5程序正確性證明－Hoare的公理化方法Hoare提出的公理和相應(yīng)控制語句的證明規(guī)則。3.循環(huán)語句規(guī)則 P=>I,{I∧R}S{I},I∧﹁R=>Q {P}WHILERDOS

{Q} 此規(guī)則中的邏輯表達(dá)式I就是非形式證明中的循環(huán)不變式斷言。條件P=>I表明，當(dāng)控制進(jìn)入循環(huán)時(shí)，循環(huán)不變式I應(yīng)為真；不變式{I∧R}S{I}表明，如果執(zhí)行S之前（R為真時(shí)才執(zhí)行S）I為真，且S執(zhí)行終止，則S執(zhí)行后I仍為真；條件I∧﹁R=>Q表明，如果控制退出循環(huán)，Q應(yīng)為真。2.5程序正確性證明－Hoare的公理化方法Hoare提出的公理和相應(yīng)控制語句的證明規(guī)則。4.并置規(guī)則 {P}S1{R},{R}S2{Q} {P}S1;S2{Q}2.5程序正確性證明－Hoare的公理化方法Hoare提出的公理和相應(yīng)控制語句的證明規(guī)則。4.結(jié)論規(guī)則 P=>R,{R}S{Q} {P}S{Q} 或 {P}S{R},R=>Q {P}S{Q}2.5程序正確性證明－Hoare的公理化方法舉例：說明公理化證明程序部分正確性的方法。將該例的輸入斷言，循環(huán)不變式斷言和輸出斷言插入程序中相應(yīng)位置，則程序體為：STARTI(x):{x0≥0∧y0≥0∧(x0≠0∨y0≠0)}/*輸入斷言*/(x,y)←(x0,y0);/*x:=x0,y:=y0的縮寫*/WHILEx≠0DOL(x,y):{x≥0∧y≥0∧(x≠0∨y≠0)=>gcd(x,y)=gcd(x0,y0)}/*循環(huán)不變式*/IFy≥xTHENy←y-xELSE(s,x,y)←(x,y,s)z:=y;O(x,z):{z=gcd(x0,y0)}

/*輸出斷言*/

2.5程序正確性證明－Hoare的公理化方法要證明程序P是部分正確的，則要證明目標(biāo)Goal是部分正確的。Goal:{x0≥0∧y0≥0∧(x0≠0∨y0≠0)} BodyP /*體為賦值語句與WHILE-DO的并*/ {z=gcd(x0,y0)}2.5程序正確性證明－Hoare的公理化方法1.按并置規(guī)則 根據(jù)并置規(guī)則分解Goal，需證明兩個(gè)不變式語句

Goal1:{x0≥0∧y0≥0∧(x0≠0∨y0≠0)} (x,y)←(x0,y0) L(x,y):{x0≥0∧y0≥0∧(x0≠0∨y0≠0)=>gcd(x,y)=gcd(x0,y0}

Goal2:L(x,y) WHILEx≠0DOS; O(x,y):{z=gcd(x0,y0)}2.5程序正確性證明－Hoare的公理化方法2.由賦值公理證Goal1，只需證明邏輯表達(dá)式

Log1:x0≥0∧y0≥0∧(x0≠0∨y0≠0)=>L(x0,y0)2.5程序正確性證明－Hoare的公理化方法3.使用WHILE-DO規(guī)則證明Goal2。根據(jù)WHILE規(guī)則，可取I為L(zhǎng)(x,y)，則顯然L(x,y)=>I，于是有：

Goal3:{L(x,y)∧x≠0} IFy≥0THEN...ELSE...{L(x,y)}2.5程序正確性證明－Hoare的公理化方法4.由x=0，執(zhí)行z←y分支，需證明邏輯表達(dá)式：

Log2:L(x,y)∧x=0)=>z=gcd(x0,y0)

2.5程序正確性證明－Hoare的公理化方法5.根據(jù)條件規(guī)則，為了證明Goal3，則需證明：

Goal4:{L(x,y)∧x≠0∧y≥x}y←y-x{L(x,y)}

Goal5:{L(x,y)∧x≠0∧y<x}(s,x,y)←(x,y,s){L(x,y)}

2.5程序正確性證明－Hoare的公理化方法6.根據(jù)賦值公理，為了證明Goal4、Goal5，只需證明表達(dá)式：Log3:L(x,y)∧x≠0∧y≥x)=>L(x,y-x)Log4:L(x,y)∧x≠0∧y<x)=>L(y,x)推理演繹樹因此，證明Goal歸結(jié)為證明落及表達(dá)式Log1,Log2,Log3,Log4。這四個(gè)邏輯表達(dá)式正好是Floyd證明方法中的四個(gè)驗(yàn)證條件，證明過程省略。討論：利用Hoare的公理化方法證明下述程序的部分正確性。

2.5程序正確性證明－良序集方法（證明程序終止性）R.W.Floyd在1967年提出來的。設(shè)程序P的輸入斷言為φ(x)，利用良序集方法證明P關(guān)于φ(x)是終止的可按以下步驟進(jìn)行：1.選取一個(gè)點(diǎn)集去截?cái)喑绦虻母鱾€(gè)循環(huán)部分，并且在每一截?cái)帱c(diǎn)i處建立一個(gè)中間斷言qi(x,y)。程序就被分解為若干條通路，同時(shí)規(guī)定每一條通路都不包含有中間截?cái)帱c(diǎn)；2.選取一個(gè)良序集(W,)，并且在每一截?cái)帱c(diǎn)i處定義一個(gè)終止表達(dá)式Ei(x,y)；3.證明所選取的斷言是“良斷言”。即滿足：1）若對(duì)于每一個(gè)從程序入口到斷點(diǎn)i的通路α有：φ(x)∧Rα(x,y)=>qi(x,rα(x,y))2）若對(duì)于每一個(gè)由斷點(diǎn)i到斷點(diǎn)j的通路α有：qi(x,y)∧Rα(x,y)=>qj(x,rα(x,y))這里，Rα和rα分別表示通過通路α的條件及通過通路α后變量y的值。4.證明終止表達(dá)式是“良函數(shù)”。即對(duì)于每個(gè)斷點(diǎn)i有qi(x,y)=>Ei(x,y)∈W5.證明終止條件成立。即對(duì)每一條從斷點(diǎn)i到斷點(diǎn)j，并且為某個(gè)循環(huán)的一部分的通路α有：qi(x,y)∧Rα(x,y)=>[Ei(x,y)Ej(x,rα(x,y))??良序集：設(shè)(W,)是一個(gè)偏序集（滿足傳遞、反對(duì)稱和反自反性），如果不存在由W中的元素構(gòu)成的無限遞減序列a0a1a2…則稱(W,)為良序集。????例：另一個(gè)計(jì)算兩個(gè)正整數(shù)x1,x2的最大公約數(shù)的程序。輸入、輸出斷言為：φ(x):x1>0∧x2>0Ψ(x,z):z=gcd(x1,x2)終止性證明1）在Ｂ，Ｃ點(diǎn)將循環(huán)斷開，并在這兩點(diǎn)分別建立中間斷言。2）取良序集為(N,<)，并在Ｂ、Ｃ點(diǎn)分別建立終止表達(dá)式。3）證明中間斷言是良斷言。由于循環(huán)由Ｂ，Ｃ點(diǎn)斷開后，程序分解為７條通路，因此需分別對(duì)前６條通路予以證明。（通路Ｃ－>Ｈ與證明終止性無關(guān)）4）證明終止表達(dá)式是良函數(shù)。5）證明終止條件成立。即對(duì)與循環(huán)有關(guān)的通路展開證明。1）在Ｂ，Ｃ點(diǎn)將循環(huán)斷開，并在這兩點(diǎn)分別建立中間斷言。qB(x,y):y1>0∧y2>0qC(x,y):y1>0∧y2>02）取良序集為(N,<)，并在Ｂ、Ｃ點(diǎn)分別建立終止表達(dá)式。EB(x,y):y1EC(x,y):y1+2y23）證明中間斷言是良斷言。由于循環(huán)由Ｂ，Ｃ點(diǎn)斷開后，程序分解為７條通路，因此需分別對(duì)前６條通路予以證明。（通路Ｃ－>Ｈ與證明終止性無關(guān)）1.通路α1(AB)φ(x)=>qB(x,y)qB(x,x1,x2,1)即：x1>0∧x2>0=>x1>0∧x2>0

3）證明中間斷言是良斷言。由于循環(huán)由Ｂ，Ｃ點(diǎn)斷開后，程序分解為７條通路，因此需分別對(duì)前６條通路予以證明。（通路Ｃ－>Ｈ與證明終止性無關(guān)）2.通路α2(BDB)qB(x,y)

∧y1是偶數(shù)∧y2是偶數(shù)=>qB(x,y)qB(x,y1/2,y2/2,2y3)即：y1>0∧y2>0∧y1是偶數(shù)∧y2是偶數(shù)=>y1/2>0∧y2/2>0

3）證明中間斷言是良斷言。由于循環(huán)由Ｂ，Ｃ點(diǎn)斷開后，程序分解為７條通路，因此需分別對(duì)前６條通路予以證明。（通路Ｃ－>Ｈ與證明終止性無關(guān)）3.通路α3(BEB)qB(x,y)

∧y1是偶數(shù)∧y2是奇數(shù)=>qB(x,y)qB(x,y1/2,y2,y3)即：y1>0∧y2>0∧y1是偶數(shù)∧y2是奇數(shù)=>y1/2>0∧y2>0

3）證明中間斷言是良斷言。由于循環(huán)由Ｂ，Ｃ點(diǎn)斷開后，程序分解為７條通路，因此需分別對(duì)前６條通路予以證明。（通路Ｃ－>Ｈ與證明終止性無關(guān)）4.通路α4(BＣ)qB(x,y)

∧y1是奇數(shù)=>qC(x,y)即：y1>0∧y2>0∧y1是奇數(shù)=>y1>0∧y2>0

3）證明中間斷言是良斷言。由于循環(huán)由Ｂ，Ｃ點(diǎn)斷開后，程序分解為７條通路，因此需分別對(duì)前６條通路予以證明。（通路Ｃ－>Ｈ與證明終止性無關(guān)）5.通路α5(CKＣ)qC(x,y)

∧y1是奇數(shù)∧y2是偶數(shù)=>qC(x,y)qC(x,y1,y2/2,y3)即：y1>0∧y2>0∧y1是奇數(shù)∧y2是偶數(shù)=>y1>0∧y2/2

>0

3）證明中間斷言是良斷言。由于循環(huán)由Ｂ，Ｃ點(diǎn)斷開后，程序分解為７條通路，因此需分別對(duì)前６條通路予以證明。（通路Ｃ－>Ｈ與證明終止性無關(guān)）6.通路α6(CGKＣ)qC(x,y)

∧y1是奇數(shù)∧y2是奇數(shù)∧y1

≠y2

=>qC(x,y)qC(x,y2,|y1-y2|/2,y3)即：y1>0∧y2>0∧y1是奇數(shù)∧y2是奇數(shù)∧y1

≠y2

=>y2>0∧|y1-y2|/2

>0

以上6個(gè)蘊(yùn)涵式都是顯然成立的。這樣就證明了qB(x,y)，qC(x,y)是良斷言。4）證明終止表達(dá)式是良函數(shù)。qB(x,y)=>EB(x,y)∈NqC(x,y)=>EC(x,y)∈N即要證y1>0∧y2>0=>y1∈Ny1>0∧y2>0=>y1+2y2∈N由于y1和y2均為整數(shù)，所以這兩個(gè)關(guān)系是顯然成立的。5）證明終止條件成立。即對(duì)與循環(huán)有關(guān)的通路展開證明。與循環(huán)有關(guān)的通路是:α2(BDB)α3(BEB)α5(CKＣ)α6(CGKＣ)分別予以證明。5）證明終止條件成立。即對(duì)與循環(huán)有關(guān)的通路展開證明。α2(BDB)qB(x,y)

∧y1是偶數(shù)∧y2是偶數(shù)=>EB(x,y1,y2,y3)>EB(x,y1/2,y2/2,2y3)即：y1>0∧y2>0∧y1是偶數(shù)∧y2是偶數(shù)=>y1>y1/25）證明終止條件成立。即對(duì)與循環(huán)有關(guān)的通路展開證明。α3(BEB)qB(x,y)

∧y1是偶數(shù)∧y2是奇數(shù)=>EB(x,y1,y2,y3)>EB(x,y1,y2/2,y3)即：y1>0∧y2>0∧y1是偶數(shù)∧y2是奇數(shù)=>y1>y1/25）證明終止條件成立。即對(duì)與循環(huán)有關(guān)的通路展開證明。α5(CKＣ)qC(x,y)

∧y1是奇數(shù)∧y2是偶數(shù)=>EC(x,y1,y2,y3)>EC(x,y1,y2/2,y3)即：y1>0∧y2>0∧y1是奇數(shù)∧y2是偶數(shù)=>y1+2y2>y1+y25）證明終止條件成立。即對(duì)與循環(huán)有關(guān)的通路展開證明。α6(CGKＣ)qC(x,y)

∧y1是奇數(shù)∧y2是奇數(shù)∧y1

≠y2

=>EC(x,y1,y2,y3)>EC(x,y2,|y1-y2|/2,y3)即：y1>0∧y2>0∧y1是奇數(shù)∧y2是奇數(shù)∧y1

≠y2

=>y1+2y2>y2+|y1-y2|上述終止條件顯然成立。這樣，即證明了程序的終止性。討論：利用良序集方法證明下述程序的終止性。

2.5程序正確性證明－Kunth的計(jì)數(shù)器方法D.E.Kunth于1968年提出了證明程序終止性的計(jì)數(shù)器方法。該方法直觀易懂，其證明過程分為三步：1.為程序中的每個(gè)循環(huán)附加一個(gè)新的變量（如i，j通常被稱為計(jì)數(shù)器），進(jìn)入該循環(huán)前計(jì)數(shù)器置0，每執(zhí)行一次循環(huán)計(jì)數(shù)器累加1；2.為每個(gè)循環(huán)設(shè)置一個(gè)中間斷言，它表明相應(yīng)的計(jì)數(shù)器不會(huì)超過某個(gè)固定的界限；3.進(jìn)一步證明第2步設(shè)置的中間斷言是不變式斷言。2.5程序正確性證明－Kunth的計(jì)數(shù)器方法舉例：對(duì)前述證明部分正確性z=gcd(x,y)的例子，用計(jì)數(shù)器方法證明其終止性。證明：輸入斷言I(x):x0≥0∧y0≥0∧(x0≠0∨y0≠0)1.引入計(jì)數(shù)器i，并根據(jù)程序語義設(shè)置斷言為：

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

即計(jì)數(shù)器i不會(huì)超過界限2x0+y0。PROGRAMgcd1;VARx,y,z,s:INTEGER;BEGINREAD(x,y);i:=0;I(x):{x0≥0∧y0≥0∧(x0≠0∨y0≠0)}WHILEx≠0DOL(x,y):{x≥0∧y≥0∧2x+y+i≤2x0+y0}BEGIN

IFy≥xTHENy←y-xELSE(s,x,y)←(x,y,s)i←i+1END;z←yEND;2.5程序正確性證明－Kunth的計(jì)數(shù)器方法證明：輸入斷言I(x):x0≥0∧y0≥0∧(x0≠0∨y0≠0)2.建立驗(yàn)證條件： 第一次到達(dá)循環(huán)語句Ｌ處，僅執(zhí)行了賦值語句：x=x0;y=y0;i:=0;

C1(x,y):[x0≥0∧y0≥0∧(x0≠0∨y0≠0)] =>[x0≥0∧y0≥0∧2x0+y0+0≤2