8Hoare的公理化方法

8.Hoare的公理化方法該方法的主要思想是給出公理系統(tǒng)，包含賦值公理規(guī)則、復(fù)合推理規(guī)則、條件推理規(guī)則、循環(huán)推理規(guī)則和推論規(guī)則。8.1Hoare邏輯和Hoare演算定義8.1 (Hoare邏輯的語(yǔ)法)令B是謂詞邏輯的基，B上的Hoare公式是形如0/S/〃的表達(dá)式，其中p,qcWFFB是謂詞邏輯里的公式，S^L2B是一個(gè)循環(huán)程序?；鵅上的Hoare公式全體記為HFB。定義8.2 (Hoare邏輯的語(yǔ)義)給定謂詞邏輯的基B，令I(lǐng)是B的一個(gè)解釋，￡是相應(yīng)的狀態(tài)集合。每個(gè)Hoare公式{p/Sfq/eHFB都被一語(yǔ)義范函，亦記為I，映射成一個(gè)函數(shù)：I({p}S{q})：￡—Bool，此函數(shù)定義為：對(duì)于矣￡，I({p}S{q})(o)=true當(dāng)且僅當(dāng)若I(p)(o)=true且％的可有定義，則有I(q)(Mi(S^(d^)=trueoRMK.每當(dāng)I(p)(。)為假或MS)?)沒(méi)定義，I({p}S{q})(o)就為真。這就是說(shuō)，“Hoare公式仞S{q}在某解釋下恒真”恰恰就是說(shuō)“S關(guān)于公式p和q是部分正確的”。程序的含義^，⑶有操作語(yǔ)義和指稱語(yǔ)義之分。與謂詞邏輯類(lèi)似，有以下符號(hào)記法：=1{p}S{q}“Hoare公式在解釋I下恒真”1={p}S{q}"Hoare公式在解釋I下邏輯恒真”W={p}S{q}"Hoare公式是公式集合W^WFFB的邏輯結(jié)果”例8.3在通常的解釋I下，Hoare公式{x〉5}x:=2*x{x>20}成真的條件是什么？對(duì)于某狀態(tài)6I({x>5}x:=2*x{x>20})(c)=trueiffI({x>5}(6)=false，或I({x>20}(M(x:=2*x)6)=trueiff6(x)<5，或M.(x:=2*x)(6)(x)>20iff6(x)<5，或(6(x)>10證明：在通常的解釋I下，％{true}whilex^10dox:=x+1od{x=10}。令whilex^10dox:=x+1od是循環(huán)程序S。根據(jù)Hoare公式的語(yǔ)義定義，只需證得：對(duì)于任意狀態(tài)6或血/6)句沒(méi)定義，或I({p}S{q})(6)為真，就足夠了。顯然要么6(x)<10，要么6(x)>10。若6(x)>10則M冏(6沒(méi)定義；若6(x)<10則M.i(S)6)(x)=10o證明：{y+1>y}={true}x:=y+1{x>y}對(duì)于任意解釋I和任意狀態(tài)6I(x>y)(M(x:=y+1)^(6))=trueiffI(x>y)(6[x/I(y+1)(6)])=trueiffI(y+1>y)(6)=true(根據(jù)代入定理)iffI是{y+1>y}的模型。8.1.1Hoare演算我們知道，演算的含義就是從已知的恒真公式（如公理）推出更多的結(jié)論（如定理）。一、賦值公理現(xiàn)在要研究的是形如{p}x:=t{q}的Hoare公式，具體要研究其中的公式p和q之間有何關(guān)系？賦值公理就是給出它們之間的具體關(guān)系。作?????????????????為例子我們來(lái)考慮{x〉0}x:=x+1{x>1}。為了便于討論，不妨把變量x的舊值（執(zhí)行前）表示為x,把新值表示為x'?，F(xiàn)在可把本例的Hoare公式視為如下公式：x>0Ax=x+1^>x>1注意，該邏輯式由三部分組成，其一是前置條件x〉0,其二是變量的新老值間的關(guān)系式，其三是后置條件x'>1，并且前置條件只含老值x，而后置條件只含新值x'。新舊關(guān)系式中即包含新值也包含舊值。從上述分析不難看到，如果從新老值的關(guān)系式求出新值，并將它代入到后置條件里，x+1>1，則會(huì)得到只由老值組成的前置條件；同樣，如果從新老值的關(guān)系式中求出老值，并將它代入到前置條件中，x-1>0，則會(huì)得到只由新值組成的后置條件式。這就是從前置條件求后置條件和從后置條件求前置條件的問(wèn)題。這里的一個(gè)關(guān)鍵問(wèn)題是，如何從新老值的等式求出新值或老值。顯然，求新值是非常簡(jiǎn)單的事情，因此，從后置條件求前置條件是較容易的事情；但想從前置條件求后置條件，有時(shí)并不那么容易，因?yàn)檫@時(shí)需.? .??????????????????????.要通過(guò)求反函數(shù)的方法來(lái)求老值。如果反函數(shù)是容易求到的，那么從前置條件求后置條件也變成容易的事情。據(jù)上述討論，我們不難理解所給出的下面賦值公理。I(i)賦值公理"}x:=t{p}對(duì)于所有peWFFB，xeV，tcTB。這條公理正是采用了從后置條件求前置條件的思路。考慮下面幾個(gè)驗(yàn)證公式：{x=0}x:=x+1{x=1}{x>0}x:=x+1{x>1}{x>0}x:=x+1{x>0}{x>0}y:=x+1{x>0ny>1}它們都是恒真的Hoare公式，即前面均可帶上“”。但它們并不都可從賦值公理直接導(dǎo)出(其中的公式3)不能從賦值公理直接導(dǎo)出)。二、復(fù)合語(yǔ)句規(guī)則考慮形如{p}，/以〃的驗(yàn)證公式。顯然，如果存在某個(gè),，使公式{p}S]{〃和{r}S2{q}成立，則在S]的入口處p的成立，能保證在，2的出口處q的成立。故復(fù)合語(yǔ)句的規(guī)則可如下：復(fù)合語(yǔ)句規(guī)則{p}S"},{r)S2{q) 對(duì)于所有p,q,reWFFB,，追乳：{p}S1；S2{q}三、條件語(yǔ)句規(guī)則考慮形如{p}(fethenS1elseS2f{q}的Hoare公式。條件語(yǔ)句將產(chǎn)生一條相應(yīng)的推理規(guī)則，稱之為條件規(guī)則。從條件語(yǔ)句的入口到出口的路有兩條，一是條件表達(dá)式e為真的路，一是e為假的路。經(jīng)過(guò)這兩條路的條件分別為pAe和pAf。故如果有：pAe^q和pA—e^>q則在出口處q自然成立。條件語(yǔ)句規(guī)則{pAe}S{q},{pA—e}S2{q} 對(duì)于所有p,q^WFFB,e^QFFB,S1,S2^L2B{p}ifethenS1elseS2fi{q}四、循環(huán)語(yǔ)句規(guī)則最后考慮循環(huán)語(yǔ)句的規(guī)則。假設(shè)有循環(huán)語(yǔ)句whileedoSod，令當(dāng)前狀態(tài)為6則循環(huán)的執(zhí)行過(guò)程是：(用b)計(jì)算e的值；檢查它是否為真？若為真則執(zhí)行S并重復(fù)執(zhí)行上述過(guò)程；若為假，則循環(huán)將終止。由此可知在循環(huán)的出口處條件—e一定滿足，即它是后置條件中的一部分。另外我們還能注意到，如果有一斷言〃滿足“在執(zhí)行循環(huán)體之前p成立，則執(zhí)行S后p仍然成立”，即有性質(zhì)0△荷s{p}，則在循環(huán)的出口處p也成立。根據(jù)上述討論，可給出下面所示的循環(huán)語(yǔ)句規(guī)則。（iv）循環(huán)語(yǔ)句規(guī)則{pES{p} 對(duì)于所有p^WFFB,KQFFB,SeL2b{p}whileedoSod{p^—e}五、推論規(guī)則假設(shè)已知公式{p}S{g}成立，并且有qpq，p^p，即可以強(qiáng)化前置條件，或可以弱化后置條件，則新的公式{p'}S{q'}更應(yīng)該成立。于是可給出下面所示的一條推論規(guī)則。（V）推論規(guī)則PDp，{p}S{q},qnq 對(duì)于所有p,q,p,q，wWFFB,SeL2B{p}S{q'}派生規(guī)則(derivedrule):若存在從謂詞邏輯所有的邏輯恒真公式和{S1,…,sj到s的一個(gè)演繹，則稱是一條I：上派生規(guī)則。s:(I)對(duì)于所有p,qcWFFB，xGV，teTB，PF；{p}；：=t{q}(II)對(duì)于所有p°…,p.cWFFBS1,…,Sn^L2B(n>2){PjS1{p}{p}S2"???，%}Sn{p}{p0}S『…;Sn{pn}(III) 對(duì)于所有p,q,r^WFF,e^QFF.Sd尹B B 2pnr,{r/\e}S{r},(rA^e)^>q{p}whileedoSod{q}定義(循環(huán)不變式)設(shè)whileedoSod是循環(huán)語(yǔ)句，e^QFFB，且有{me}S{r}則稱r為該循環(huán)語(yǔ)句的不變式(invariant)。定理(循環(huán)不變式的合取式也是一個(gè)循環(huán)不變式)若r和r'是whileedoSod的循環(huán)不變式，則rAr'是循環(huán)不變式。證明：只需證明"Re}S{rAr'}°(這是比較直觀的問(wèn)題，但又不是顯然的問(wèn)題，這需要證明，因?yàn)樵趶?qiáng)化前置條件的同時(shí)強(qiáng)化了后置條件)。具體證明：任一不等于④的b都使下式成立：I(rAr'Ae)bdI(rAr')(M.(S)(b))RMK.這里要注意的有兩點(diǎn)：一是循環(huán)不變式并不保證執(zhí)行循環(huán)體之前一定??????????????????成立，它只保證“如果在執(zhí)行循環(huán)體之前成立，則執(zhí)行后也成立”。??二是循環(huán)不變式可有無(wú)窮多個(gè)。當(dāng)證明程序時(shí)需要找夠證明程序正確性的合適的循環(huán)不變式，當(dāng)然不一定唯一。定義(合適循環(huán)不變式)設(shè)r是循環(huán)語(yǔ)句whileedoSod的一個(gè)循環(huán)不變式。如若還滿足條件pDr和rA—ieDg，則稱r為公式{p}whileedoSod{g}的合適循環(huán)不變式。RMK.其中第一條表示入口處若p成立，則r也成立；第二條表示r要強(qiáng)到rA—e能蘊(yùn)含g的程度。定義(Hoare公理系統(tǒng))由以上賦值公理、復(fù)合推理規(guī)則、條件推理規(guī)則、循環(huán)推理規(guī)則和推論規(guī)則所組成的公理系統(tǒng)稱之為Hoare公理系統(tǒng)。8.2可靠性與相對(duì)完備性定理8.5(可靠性，soundness)令B是謂詞邏輯的基。對(duì)于任意公式集W^WFFB和HFB中的任意公式{p}S{q}(滿足p,qeWFFB和SeL2B)，若W{p}S/q}，則有Wl={p}S{q}。證明：(使用循環(huán)程序的指稱語(yǔ)義)賦值公理(略)。復(fù)合語(yǔ)句規(guī)則(略)。條件語(yǔ)句規(guī)則。假設(shè)巳^^足四}和1=//pZ}S2{q}。為了要證明1=//p}ifethenS1elseS2f/q}，令b是任意一個(gè)不同于④的狀態(tài)，且滿足I(p)(b)=true。根據(jù)定義5.17和定義5.19，M.^(ifethenS1elseS2fi)(b)=if-then-else(I(e)(b),Mf(S1)(b),M^(S2)(b))，若Mj(ifethenS1elseSJi)(b)沒(méi)有定義，則結(jié)論得證；否則，分成兩種情況:(1)I(e)(b)=true且M.^(ifethenS1elseS2fi)(b)=M.^(S1)(b)^^o(2)I(e)(b)=false且M^(ifethenS1elseS2fi)(b)=M.^(S2)(b)^^o對(duì)于情況(1)，I(p八e)(b)=true。又根據(jù)已知1=//p^e}S1/q}，所以I(q)(M?(S1)(b))=true。對(duì)于情況(2)，I(pn「e)(b)=true。又根據(jù)已知'「{p^pSJq}，所以I(q)(M『(S2)(b))=true。循環(huán)語(yǔ)句規(guī)則。假設(shè) f/pne}S{p} (1)往證\=Jp}whileedoSod{pA^e}；或等價(jià)地說(shuō)，對(duì)于所有的狀態(tài)興￡,若I(p)(o)=true，且M(whileedoSod)((^)有定義，' > (2)則有I(pA^e)(M(whileedoSod)，))=true。根據(jù)定義5.17，M(whileedoSod)是如下定義的范函中:［Z?—Z?］T［筆—孔］的最小不動(dòng)點(diǎn)，Iif-then-else(I(e)(o),f(^^(S1)(o),b)) 若b壬①o 若b=O要證性質(zhì)(2)成立，就要保證最小不動(dòng)點(diǎn)是一個(gè)可納謂詞。為此需要如下這樣一個(gè)引理：引理8.6(部分正確性是可納謂詞)令^,^:Y^Bool是謂詞。那么如下定義的謂詞兀:("禮)—Bool是可納的(admissible)：Nf)=trueiff對(duì)于所有的狀態(tài)b。，若?(。)=true且f(b)^o^^(f(b))=true。證明：令S是［知—知］中的一條鏈，滿足，對(duì)于S中的所有函數(shù)f，都有兀(f)=true。為了證明k(uS)=true，令狀態(tài)bfZ滿足?(b)=true和(^S)(b)=b'，o。因?yàn)楦鶕?jù)定理4.3,(^S)(b)=^S(b)，容易得到^(b)=true。又因?yàn)槿缡且粋€(gè)平完全半序集，一定有，S中至少存在一個(gè)函數(shù)f滿足f(b)=b'。因兀(f)=true，^(bf)=true，所以k(uS)=true。□卜面繼續(xù)循環(huán)規(guī)則的證明。令兀如引理8.6所定義的一樣，令^=I(p)且^=I(pA^e)，于是要證明的性質(zhì)(2)就變成了(3)兀(日中)=true (3)根據(jù)引理8.6我們可以使用Scott歸納原理(即不動(dòng)點(diǎn)定理中所使用的歸納法)：(歸納基礎(chǔ))n(l)=true(歸納步)假設(shè)對(duì)于所有的函數(shù)gw[￡t￡]都滿足n(g)=true。令某 M?%?①??/:...?、'? ??函數(shù)fc[￡尸禮]滿足兀(f)=true。為了證明n(^(f))=true，令b0G￡滿足下面的條件(4)和(5)：TOC\o"1-5"\h\zI(p)30)=true (4)和^(f)(^0))，④ (5)有必要證得，I(p^-e)(^(f)(^)) (6)情況(1)：I(e)(%)=true。那么^(f)(^0)=f(M^(S1)(oo))，結(jié)合(5)就有 f(^^(S1)(o))。④ (7)fM^^(S1)