第3章-程序的正確性證明

第三章程序的正確性證明主要內(nèi)容程序的測試Floyd-Hoare規(guī)則公理方法Dijkstra最弱前置條件方法程序的正確性所謂一段程序是正確的，是指這段程序能準(zhǔn)確無誤地完成編寫者所期望賦予它的功能?；蛘哒f，對(duì)任何一組允許的輸入信息，程序執(zhí)行后能得到一組和這組輸入信息相對(duì)應(yīng)的正確的輸出信息。通俗地說，“做了它該做的事，沒有做它不該做的事”一段程序是錯(cuò)誤的，是指：（1）程序完成的事情并不是程序員想要完成的事情；（2）程序員想要程序完成的事情，程序并沒有完成。一般來說，程序中含有錯(cuò)誤是很難避免的。錯(cuò)誤可能有：（1）設(shè)計(jì)時(shí)的錯(cuò)誤；（2）程序編寫時(shí)的錯(cuò)誤；（3）運(yùn)行時(shí)的錯(cuò)誤等。發(fā)現(xiàn)錯(cuò)誤或盡量減少錯(cuò)誤，是程序設(shè)計(jì)人員的努力方向，更是其職責(zé)。如何保證程序的正確性要求1、從編程時(shí)就應(yīng)該盡量地避免和減少錯(cuò)誤的發(fā)生2、當(dāng)程序編好后要盡量找出錯(cuò)誤，糾正錯(cuò)誤避免錯(cuò)誤的方法

1、程序的結(jié)構(gòu)要簡單2、采用標(biāo)準(zhǔn)的軟件設(shè)計(jì)工具、標(biāo)準(zhǔn)的算法手冊以及有效的程序設(shè)計(jì)方法發(fā)現(xiàn)錯(cuò)誤的方法

1、利用測試工具:跟蹤程序的運(yùn)行，用測試的辦法去查找并發(fā)現(xiàn)程序錯(cuò)誤；2、利用程序的驗(yàn)證系統(tǒng)：證明程序的正確性。程序測試：給程序一組或幾組初始值進(jìn)行試運(yùn)行，將運(yùn)行的結(jié)果與實(shí)現(xiàn)已知的結(jié)果比較，若兩則相同，則認(rèn)為程序是正確的，若兩則不同，則說明程序有錯(cuò)誤。一、程序測試軟件測試的目的基于不同的立場，存在著兩種完全不同的測試目的。從用戶的角度出發(fā)，普遍希望通過軟件測試暴露軟件中隱藏的錯(cuò)誤和缺陷，以考慮是否可接受該產(chǎn)品。從軟件開發(fā)者的角度出發(fā)，則希望測試成為表明軟件產(chǎn)品中不存在錯(cuò)誤的過程，驗(yàn)證該軟件已正確地實(shí)現(xiàn)了用戶的要求，確立人們對(duì)軟件質(zhì)量的信心。程序測試1983年IEEE提出的軟件工程術(shù)語中給軟件測試下的定義是：“使用人工或者自動(dòng)手段來運(yùn)行或測定某個(gè)系統(tǒng)的過程，其目的在于檢驗(yàn)它是否滿足規(guī)定的需求或是弄清預(yù)期結(jié)果與實(shí)際結(jié)果之間的差別?！睖y試是程序的執(zhí)行過程，目的在于發(fā)現(xiàn)錯(cuò)誤。一個(gè)好的測試用例在于能發(fā)現(xiàn)至今未發(fā)現(xiàn)的錯(cuò)誤；一個(gè)成功的測試是發(fā)現(xiàn)了至今未發(fā)現(xiàn)的錯(cuò)誤的測試。測試的原則1.應(yīng)當(dāng)“盡早地和不斷地進(jìn)行軟件測試”。2.測試用例應(yīng)由測試輸入數(shù)據(jù)和對(duì)應(yīng)的預(yù)期輸出結(jié)果組成。3.程序員應(yīng)避免檢查自己的程序。4.在設(shè)計(jì)測試用例時(shí)，應(yīng)當(dāng)包括合理的輸入條件和不合理的輸入條件。5.充分注意測試中的群集現(xiàn)象。即測試后程序中殘存的錯(cuò)誤數(shù)目與該程序中已發(fā)現(xiàn)的錯(cuò)誤數(shù)目成正比。6.嚴(yán)格執(zhí)行測試計(jì)劃，排除測試的隨意性。7.應(yīng)當(dāng)對(duì)每一個(gè)測試結(jié)果做全面檢查。8.妥善保存測試計(jì)劃，測試用例，出錯(cuò)統(tǒng)計(jì)和最終分析報(bào)告，為維護(hù)提供方便。程序測試實(shí)質(zhì)上只是一種抽樣檢查測試過程：選取測試數(shù)據(jù)→執(zhí)行程序→輸入測試數(shù)據(jù)→記錄執(zhí)行結(jié)果→手工核對(duì)結(jié)果因此，測試只是一種查錯(cuò)的手段，它可以幫助人們?nèi)グl(fā)現(xiàn)程序中的錯(cuò)誤，但不能證明程序中沒有錯(cuò)誤，即：測試不能證明程序是正確的

程序測試的過程…軟件測試方法軟件測試的方法和技術(shù)是多種多樣的。對(duì)于軟件測試技術(shù)，根據(jù)不同角度，可以將測試方法分為不同種類。（1）從是否需要執(zhí)行被測軟件的角度，可以分為靜態(tài)測試和動(dòng)態(tài)測試；（2）從測試是否針對(duì)系統(tǒng)內(nèi)部結(jié)構(gòu)和具體實(shí)現(xiàn)算法的角度，可以分為白盒測試和黑盒測試；（3）從實(shí)際測試的前后過程來看，軟件測試是由一系列的不同測試組成，這些步驟可以分為：單元測試、組裝測試（集成測試）、確認(rèn)測試和系統(tǒng)測試。兩種重要的軟件測試方法

黑盒測試這種方法是把測試對(duì)象看做一個(gè)黑盒子，測試人員完全不考慮程序內(nèi)部的邏輯結(jié)構(gòu)和內(nèi)部特性，只依據(jù)程序的需求規(guī)格說明書，檢查程序的功能是否符合它的功能說明。黑盒測試又叫做功能測試或數(shù)據(jù)驅(qū)動(dòng)測試。

白盒測試此方法把測試對(duì)象看做一個(gè)透明的盒子，它允許測試人員利用程序內(nèi)部的邏輯結(jié)構(gòu)及有關(guān)信息，設(shè)計(jì)或選擇測試用例，對(duì)程序所有邏輯路徑進(jìn)行測試。通過在不同點(diǎn)檢查程序的狀態(tài)，確定實(shí)際的狀態(tài)是否與預(yù)期的狀態(tài)一致。因此白盒測試又稱為結(jié)構(gòu)測試或邏輯驅(qū)動(dòng)測試。黑盒測試方法是在程序接口上進(jìn)行測試，主要是為了發(fā)現(xiàn)以下錯(cuò)誤:是否有不正確或遺漏了的功能?在接口上，輸入能否正確地接受?能否輸出正確的結(jié)果?是否有數(shù)據(jù)結(jié)構(gòu)錯(cuò)誤或外部信息(例如數(shù)據(jù)文件)訪問錯(cuò)誤?性能上是否能夠滿足要求?是否有初始化或終止性錯(cuò)誤?用黑盒測試發(fā)現(xiàn)程序中的錯(cuò)誤，必須在所有可能的輸入條件和輸出條件中確定測試數(shù)據(jù)，來檢查程序是否都能產(chǎn)生正確的輸出。但這是不可能的。假設(shè)一個(gè)程序P有輸入量X和Y及輸出量Z。在字長為32位的計(jì)算機(jī)上運(yùn)行。若X、Y取整數(shù)，按黑盒方法進(jìn)行窮舉測試：可能采用的測試數(shù)據(jù)組：232×232＝264

如果測試一組數(shù)據(jù)需要1毫秒，一年工作365×24小時(shí)，完成所有測試需5億年。

軟件人員使用白盒測試方法，主要想對(duì)程序模塊進(jìn)行如下的檢查：對(duì)程序模塊的所有獨(dú)立的執(zhí)行路徑至少測試一次；對(duì)所有的邏輯判定，取“真”與取“假”的兩種情況都至少測試一次；在循環(huán)的邊界和運(yùn)行界限內(nèi)執(zhí)行循環(huán)體；測試內(nèi)部數(shù)據(jù)結(jié)構(gòu)的有效性；對(duì)一個(gè)具有多重選擇和循環(huán)嵌套的程序，不同的路徑數(shù)目可能是天文數(shù)字。給出一個(gè)小程序的流程圖，它包括了一個(gè)執(zhí)行20次的循環(huán)。包含的不同執(zhí)行路徑數(shù)達(dá)520條，對(duì)每一條路徑進(jìn)行測試需要1毫秒，假定一年工作365×24小時(shí)，要想把所有路徑測試完，需3170年。即使能完成這樣的測試，也不意味差程序沒有錯(cuò)誤。如：x=x+z,錯(cuò)誤寫成x=x-z,且當(dāng)z=0時(shí)，這種錯(cuò)誤仍然難以發(fā)現(xiàn)

。測試常常是不充分的，它只能發(fā)現(xiàn)某些錯(cuò)誤存在，而不能證明錯(cuò)誤的不存在

。…黑盒測試

等價(jià)類劃分

邊界值分析

錯(cuò)誤推測法

因果圖例子某個(gè)TRIANGLE程序，用3個(gè)整數(shù)表示一個(gè)三角形的3條邊長。當(dāng)輸入3個(gè)整數(shù)后，該程序輸出一個(gè)結(jié)果，指出這三角形是等腰，等邊，還是不等邊三角形。這個(gè)例子只知程序的功能，而不知內(nèi)部的邏輯與結(jié)構(gòu)。在選擇數(shù)據(jù)組來測試程序時(shí)，我們可以憑經(jīng)驗(yàn)，考慮如下情況：1）合理構(gòu)成等腰三角形2）合理構(gòu)成等邊三角形3）合理構(gòu)成不等邊三角形4）等腰三角形的三種排列5）三個(gè)正數(shù)，其中兩個(gè)數(shù)之和等于第三個(gè)數(shù)6）兩邊之和等于第三邊的三種排列7）三個(gè)正數(shù)，其中兩個(gè)數(shù)之和小于第三個(gè)數(shù)8）兩邊之和小于第三邊的三種排列9）輸入三個(gè)數(shù)，其中含有010）輸入三個(gè)數(shù)，其中含有負(fù)數(shù)11）輸入三個(gè)數(shù)，其中含有非整數(shù)值12）輸入三個(gè)均為0的數(shù)13）輸入三個(gè)均為非法字符列出各種產(chǎn)生的情況來測試的方法顯然是黑盒子方法。它不關(guān)心盒子內(nèi)程序的具體邏輯，只是根據(jù)程序功能來設(shè)計(jì)測試用例等價(jià)類劃分①有效等價(jià)類：是指對(duì)于程序的規(guī)格說明來說，是合理的，有意義的輸入數(shù)據(jù)構(gòu)成的集合。②無效等價(jià)類：是指對(duì)于程序的規(guī)格說明來說，是不合理的，無意義的輸入數(shù)據(jù)構(gòu)成的集合。

例如，在程序的規(guī)格說明中，對(duì)輸入條件有一句話：“……項(xiàng)數(shù)可以從1到999……”，則有效等價(jià)類是“1≤項(xiàng)數(shù)≤999”兩個(gè)無效等價(jià)類是“項(xiàng)數(shù)＜1”或“項(xiàng)數(shù)＞999”。在數(shù)軸上表示成:

邊界值分析

人們從長期的測試工作經(jīng)驗(yàn)得知，大量的錯(cuò)誤是發(fā)生在輸入或輸出范圍的邊界上，而不是在輸入范圍的內(nèi)部。因此針對(duì)各種邊界情況設(shè)計(jì)測試用例，可以查出更多的錯(cuò)誤。比如，在做三角形計(jì)算時(shí)，要輸入三角形的三個(gè)邊長：A、B和C。我們應(yīng)注意到這三個(gè)數(shù)值應(yīng)當(dāng)滿足

A＞0、B＞0、C＞0、A＋B＞C、A＋C＞B、B＋C＞A，才能構(gòu)成三角形。但如果把六個(gè)不等式中的任何一個(gè)大于號(hào)“＞”錯(cuò)寫成大于等于號(hào)“≥”，那就不能構(gòu)成三角形。問題恰出現(xiàn)在容易被疏忽的邊界附近。使用邊界值分析方法設(shè)計(jì)測試用例，首先應(yīng)確定邊界情況。應(yīng)當(dāng)選取正好等于，剛剛大于，或剛剛小于邊界的值做為測試數(shù)據(jù)，而不是選取等價(jià)類中的典型值或任意值做為測試數(shù)據(jù)。錯(cuò)誤推測法人們也可以靠經(jīng)驗(yàn)和直覺推測程序中可能存在的各種錯(cuò)誤，從而有針對(duì)性地編寫檢查這些錯(cuò)誤的例子。這就是錯(cuò)誤推測法。錯(cuò)誤推測法的基本想法是：列舉出程序中所有可能有的錯(cuò)誤和容易發(fā)生錯(cuò)誤的特殊情況，根據(jù)它們選擇測試用例。因果圖如果在測試時(shí)必須考慮輸入條件的各種組合，可使用一種適合于描述對(duì)于多種條件的組合，相應(yīng)產(chǎn)生多個(gè)動(dòng)作的形式來設(shè)計(jì)測試用例，這就需要利用因果圖。把輸入條件視為“因”，把輸出條件視為“果”，將黑盒看成是從因到果的網(wǎng)絡(luò)圖，采用邏輯圖的形式來表達(dá)功能說明書中輸入條件的各種組合與輸出的關(guān)系。根據(jù)這種關(guān)系可選擇高效的測試用例。因果圖是一種形式化語言，是一種組合邏輯網(wǎng)絡(luò)圖。因果圖方法最終生成的就是判定表。它適合于檢查程序輸入條件的各種組合情況?！瓕?shí)例…用因果圖生成測試用例的基本步驟(1)分析軟件規(guī)格說明描述中，哪些是原因(即輸入條件或輸入條件的等價(jià)類)，哪些是結(jié)果(即輸出條件)，并給每個(gè)原因和結(jié)果賦予一個(gè)標(biāo)識(shí)符。(2)分析軟件規(guī)格說明描述中的語義，找出原因與結(jié)果之間，原因與原因之間對(duì)應(yīng)的是什么關(guān)系?根據(jù)這些關(guān)系，畫出因果圖。(3)由于語法或環(huán)境限制，有些原因與原因之間，原因與結(jié)果之間的組合情況不可能出現(xiàn)。為表明這些特殊情況，在因果圖上用一些記號(hào)標(biāo)明約束或限制條件。(4)把因果圖轉(zhuǎn)換成判定表。(5)把判定表的每一列作為依據(jù)，設(shè)計(jì)測試用例?！瓕?shí)例…在因果圖中出現(xiàn)的基本符號(hào)通常在因果圖中用Ci表示原因，用Ei表示結(jié)果，各結(jié)點(diǎn)表示狀態(tài)，可取值“0”或“1”?！?”表示某狀態(tài)不出現(xiàn)，“1”表示某狀態(tài)出現(xiàn)。主要的原因和結(jié)果之間的關(guān)系有：…實(shí)例…表示約束條件的符號(hào)為了表示原因與原因之間，結(jié)果與結(jié)果之間可能存在的約束條件，在因果圖中可以附加一些表示約束條件的符號(hào)。即a、b不能同時(shí)為1a、b中僅有一個(gè)為1a為1時(shí)，b必須為1若a為1時(shí)，則b強(qiáng)制為0a、b、c不能同時(shí)為0…實(shí)例…例如，有一個(gè)處理單價(jià)為5角錢的飲料的自動(dòng)售貨機(jī)軟件測試用例的設(shè)計(jì)。其規(guī)格說明如下：若投入5角錢或1元錢的硬幣，押下〖橙汁〗或〖啤酒〗的按鈕，則相應(yīng)的飲料就送出來。若售貨機(jī)沒有零錢找，則一個(gè)顯示〖零錢找完〗的紅燈亮，這時(shí)再投入1元硬幣并押下按鈕后，飲料不送出來而且1元硬幣也退出來；若有零錢找，則顯示〖零錢找完〗的紅燈滅，在送出飲料的同時(shí)退還5角硬幣?！薄瓕?shí)例…(1)分析這一段說明，列出原因和結(jié)果原因:1.售貨機(jī)有零錢找2.投入1元硬幣3.投入5角硬幣4.押下橙汁按鈕5.押下啤酒按鈕建立中間結(jié)點(diǎn)，表示處理中間狀態(tài)11.投入1元硬幣且押下飲料按鈕12.押下〖橙汁〗或〖啤酒〗的按鈕13.應(yīng)當(dāng)找5角零錢并且售貨機(jī)有零錢找14.錢已付清…實(shí)例…結(jié)果：21.售貨機(jī)〖零錢找完〗燈亮22.退還1元硬幣23.退還5角硬幣24.送出橙汁飲料25.送出啤酒飲料(2)畫出因果圖。所有原因結(jié)點(diǎn)列在左邊，所有結(jié)果結(jié)點(diǎn)列在右邊。(3)由于2與3，4與5不能同時(shí)發(fā)生，分別加上約束條件E。(4)因果圖…實(shí)例……實(shí)例…(5)轉(zhuǎn)換成判定表…實(shí)例程序測試的黑盒子方法常憑經(jīng)驗(yàn)進(jìn)行，在設(shè)計(jì)測試用例時(shí)可以綜合使用上述各種方法。在設(shè)計(jì)測試數(shù)據(jù)時(shí)，我們應(yīng)該考慮認(rèn)為最易出錯(cuò)和最易忽略的地方，進(jìn)行重點(diǎn)測試?！缀袦y試

邏輯覆蓋：以程序內(nèi)部的邏輯結(jié)構(gòu)為基礎(chǔ)的設(shè)計(jì)測試用例的技術(shù)。

語句覆蓋

判定覆蓋

條件覆蓋

判定－條件覆蓋

條件組合覆蓋

路徑覆蓋循環(huán)覆蓋基本路徑測試?yán)釉嚋y試下面這一程序ProcedureP(varA,B:REAL)beginif(A>1)and(B=0)thenX:=X/A;if(A=2)or(X>1)thenX:=X+1;end在執(zhí)行這個(gè)程序時(shí)，有各種不同的路徑，如：abdabedacbdacbed我們可用白盒子方法設(shè)計(jì)測試用例，其任務(wù)是盡可能多地執(zhí)行各種語句，以及調(diào)試到各種路徑。如選擇A=2,B=0,X=3則可執(zhí)行路徑acbed此時(shí)能覆蓋到全部2個(gè)計(jì)算框，可發(fā)現(xiàn)一般的語句的錯(cuò)誤這組數(shù)據(jù)可使語句都能執(zhí)行一次我們通常把這種注重語句的覆蓋叫“語句覆蓋”執(zhí)行足夠多的測試用例，使得被測程序中每個(gè)可執(zhí)行語句至少被執(zhí)行一次這種覆蓋肯定是不充分的，如：第一個(gè)判斷中and誤寫為or，第二個(gè)判斷中X>1誤寫為X>0，則無法暴露出程序的錯(cuò)誤。語句覆蓋是最弱的邏輯覆蓋準(zhǔn)則。如選擇A=3,B=0,X=1A=2,B=1,X=3則可執(zhí)行的路徑為acbdabed從所走路徑來看，上面這組數(shù)據(jù)要全面一些，它不僅通過全部兩個(gè)計(jì)算框，而且第一個(gè)判別框的兩邊都執(zhí)行過一次。我們通常把這種注重選擇測試的覆蓋叫做“判定覆蓋”，又稱為“分支覆蓋”。執(zhí)行足夠多的測試用例，使得被測程序中每個(gè)語句至少被執(zhí)行一次，且每個(gè)判斷的真假分支至少執(zhí)行一次但這組數(shù)據(jù)仍未檢查到路徑abd;第一個(gè)計(jì)算框執(zhí)行結(jié)果是否影響條件的執(zhí)行也尚未測試到。它仍不充分如選擇A=2,B=0,X=4A=1,B=1,X=1則可執(zhí)行的路徑為acbedabd從這組數(shù)據(jù)來看，它注意了4個(gè)條件A>1,B=0,A=2和X>1的覆蓋。我們稱這種注重判斷的覆蓋為“條件覆蓋”。執(zhí)行足夠多的測試用例，使得被測程序中每個(gè)判定的每個(gè)條件的可能值至少執(zhí)行一次雖然覆蓋有所改善，但對(duì)第一個(gè)判斷為真，第二個(gè)為假這一路徑acbd未測試到。它仍不充分判定/條件覆蓋執(zhí)行足夠多的測試用例，使得被測程序中的判定的每個(gè)條件的所有可能取值至少執(zhí)行一次，同時(shí)每個(gè)判定本身的所有可能判定結(jié)果至少執(zhí)行一次。是判定覆蓋與條件覆蓋的綜合，但不能保證檢查出邏輯表達(dá)式的全部錯(cuò)誤。對(duì)于上例中A>1時(shí)檢查B=0，而A<=1時(shí)，B<>0卻不去驗(yàn)證了。A=2B=0X=4;A=3,B=1,X=1兩個(gè)測試用例能同時(shí)滿足判定、條件覆蓋

以上這些數(shù)據(jù)雖然均達(dá)到一些測試目的，且各有側(cè)重，但是都是不充分的。如從條件出發(fā)，用組合的辦法使各個(gè)條件都能執(zhí)行到，則我們可以寫出以下8種條件組合：1)A>1,B=02)A>1,B<>0;(<>是不等號(hào))3)A<=1,B=04)A<=1,B<>05)A=2,X>16)A=2,X<=17)A<>2,X>18)A<>2,X<=1滿足條件組合覆蓋必滿足判定、條件、判定/條件覆蓋，但仍不能遍歷每條路徑。根據(jù)這8種條件組合，又可以優(yōu)化組成如下4組數(shù)據(jù)：A=2,B=0,X=4A=2,B=1,X=1A=1,B=0,X=2A=1,B=1,X=1它們都能使各種條件均能出現(xiàn)一次。雖然這個(gè)組合方法比較方便，邏輯也很清楚，且對(duì)執(zhí)行條件來說還是比較全面的，但是仍然又未走遍的路徑，如acbd在測試時(shí)，還要注意到計(jì)算機(jī)執(zhí)行多個(gè)條件的特點(diǎn)，即它必須把多個(gè)條件分解為簡單判別才能執(zhí)行，如上述例子可分解為右圖。

路徑覆蓋執(zhí)行足夠多的測試用例，使得被測程序中每條可能路徑至少通過一次。上例中設(shè)計(jì)測試用例:

測試用例通過ABX路徑

111abd112abed301acbd204acbed滿足路徑覆蓋保證了每個(gè)可能的路徑至少通過一次，與條件組合覆蓋結(jié)合使用可能取得較好效果。從以上兩個(gè)例子可以看出，測試通常是不充分的，它只能發(fā)現(xiàn)某些錯(cuò)誤的存在，而不能證明錯(cuò)誤的不存在。所以，在真正設(shè)計(jì)測試用例的過程種常常要考慮經(jīng)濟(jì)性，可行性。測試的關(guān)鍵就是如何設(shè)計(jì)好高效，可行的用例程序。程序測試工具美國MI公司開發(fā)的TestDirector產(chǎn)品作為測試管理流程平臺(tái)，運(yùn)用WinRunner和QuickTestProfessional作為自動(dòng)化測試工具，推薦LoadRunner作為性能測試工具。MI公司作為一個(gè)跨國型業(yè)內(nèi)專業(yè)公司，在自動(dòng)化測試方面積累了豐富的經(jīng)驗(yàn)。其測試工具作為目前測試市場的主流工具，市場占有率超過50％，從測試平臺(tái)的先進(jìn)性上來說，達(dá)到了國際上主流標(biāo)準(zhǔn)。

美國SEGUE公司的SILK系列自動(dòng)測試技術(shù)。SILK系列自動(dòng)化黑盒測試平臺(tái)能夠全面適應(yīng)電子商務(wù)技術(shù)的最新發(fā)展，具有測試自動(dòng)化，易用易維護(hù)，場景模擬精確，支持分布式測試，支持多標(biāo)準(zhǔn)協(xié)議，擴(kuò)展性強(qiáng)等優(yōu)點(diǎn)。

正確性證明測試只能發(fā)現(xiàn)程序錯(cuò)誤，但不能證明程序無錯(cuò)。原因：測試并沒有也不可能包含所有數(shù)據(jù)，只是選擇了一些具有代表性的數(shù)據(jù)，所以它具有局限性。正確性證明是通過數(shù)學(xué)技術(shù)來確定軟件是否正確，也就是說，是否符合其規(guī)格說明。正確性證明的發(fā)展二、Floyd-Hoare規(guī)則公理方法

設(shè)在程序運(yùn)行之前輸入一組X1，X2…Xn(斷言Ｐ，也稱為前斷言)，經(jīng)過S程序（語句）得到一組預(yù)定的Y1，Y2…Yn(斷言Ｑ，也稱為后斷言)，則稱程序S（語句）為正確的。用Hoare的記法，則為{P}S{Q}（一）基本規(guī)則

1）如果執(zhí)行之前P是真，執(zhí)行之后Q也是真，則記為

2）若n條路徑在語句T之前匯合，則所有前面語句Si的結(jié)論Qi都必須在邏輯上蘊(yùn)含語句T的前提P，就是說

其中，i=1,2,…,n.。

，，3)若斷言P在條件B的判斷之前成立，則判斷的兩個(gè)結(jié)論分別是

和4)若斷言P位于賦值E于變量I之后，則P中出現(xiàn)的所有I替換成E，可得到賦值的前提（稱賦值等效）。

5)凡蘊(yùn)含一語句前提的斷言，都是這個(gè)語句的前提。凡一語句結(jié)論所蘊(yùn)含的斷言，都是這個(gè)語句的結(jié)論。

上述規(guī)則將作為工具，對(duì)程序進(jìn)行驗(yàn)證。

（二）簡單語句的證明

1、空語句

2、賦值語句

{P}{P}結(jié)論即為前提

{}I:=E{P}由規(guī)則4直接得到其結(jié)論3、條件語句

來記，其中

是規(guī)則的前提，H是結(jié)論，它表示如果

為真，那么H也為真。

顯然，上述條件語句的二種形式分別可表示為{P}ifBthenS1elseS2{Q}由規(guī)則3得到{}S1{Q}和{}S2{Q}為表示方便，我們可用證明規(guī)則的一般形式

5、分情選擇語句

4、復(fù)合語句

{P}beginS1，S2，…，Snend{Q}

其中：i=1,2…,n,{Pn}={Q}L1:S1L2:S2…Ln:Snend{Q}已知：前提P為y=x2

，

D=2x-1，求順序執(zhí)行下列各語句后的結(jié)論QD:=D+2y:=y+DD:=D+2y:=y+D已知前置斷言，從前往后看：{P:y=x2

，

D=2x-1}D:=D+2

y:=y+D

D:=D+2y:=y+D

例1：

y=x2，D=2x+1y=x2+2x+1，D=2x+1y=x2+2x+1，D=2x+3y=x2+4x+4，D=2x+3Q:y=(x+2)2D=2(x+2)-1已知前提P為{P:A=A0B=B0}，求執(zhí)行語句后的結(jié)論QT:=AA:=BB:=T

從前往后證：{P:A=A0B=B0}

T:=A

A:=B

B:=T

例2：

（T=A0）（B=B0）（T=A0）（A=B0）（B=A0）（A=B0）從后往前證：{P:A=A0∧

B=B0}{B=B0∧A=A0}

T:=A

{B=B0∧T=A0}A:=B

{A=B0∧

T=A0}B:=T

{Q:A=B0∧

B=A0}例3：

{PA>0}B:=A{B>0}{B>=0}{PA<=0}B:=-A{B>=0}例4：

計(jì)算X=MAX(A,B)的程序?yàn)閕fA>=BthenX:=AelseX:=B試驗(yàn)證其正確性。

證明：{P:true}{PA>=B}X:=A{X=AX>=B}{PA<B}X:=B{X=BX>A}而X=AX>=BX=MAX(A,B)X=BX>AX=MAX(A,B)

故{P:true}ifA>=BthenX:=AelseX:=B.{X=MAX(A,B)}

求如圖所示條件語句的前提與結(jié)論{P:true}則，{true}ifA>0THENB:=AelseB:=-A{B>=0}6、循環(huán)語句

ρ稱為循環(huán)不變式：一個(gè)在每次循環(huán)的前后均為真的謂詞。

終止性：

①②{t0({0<T=t0}S{0T<t0})T(界函數(shù))

要完全正確性證明while語句，需5步

1.

Pρ2.

{ρB}S{ρ}3.

{ρB}{Q}4.

{ρB}T>05.{T=t0}S{T<t0}1)whileBdoS

例5：

求兩個(gè)自然數(shù)相除所得的商（在Q中）和余數(shù)（在R中）

{P:x>0y>0}Q:=0;R:=x;whileR>=ydobeginR:=R-y;Q:=Q+1end{Q:x=R+Q*y0<=R<yQ>=0}其中循環(huán)不變式為：{ρ:x=R+Q*yR>0Q>=0}界函數(shù)T:R

證明：(1)P={x>0y>0}Q:=0;R:=x;P1={x>0y>0Q=0R=x}(2)循環(huán)語句1.

P1ρ={x=R+Q*yR>0Q>=0}，顯然成立2.

{ρB}R:=R-y;Q:=Q+1{ρ}{ρB}{x=R+Q*yR>0Q>=0R>=y}R:=R-y{x=R+y+Q*yR>0-yQ>=0R>=y-y}{x=R+(Q+1)*yR>-yQ>=0R>=0}Q:=Q+1{x=R+Q*yR>-yQ>=0R>=0}{ρ}3.

{ρB}{Q}

{x=R+Q*yR>0Q>=0R<y}{Q:x=R+Q*y0<=R<yQ>=0}4.

{ρB}T>=0{x=R+Q*yR>0Q>=0R>=y}R>=05.

{T=t0}R:=R-y;Q:=Q+1{T<t0}{R=t0}R:=R-y;{R=t0-y}Q:=Q+1{R=t0-y<t0}T<t0{ρ:x=R+Q*yR>0Q>=0}1.

Pρ2.

{ρB}S{ρ}3.

{ρB}{Q}4.

{ρB}T>05.{T=t0}S{T<t0}2)repeat

要完全正確性證明repeat語句，需5步。

1.

Pρ2.

{ρ}S{Q}3.

{QB}{ρ}4.

{QB}{R}5.

{ρB}T>06.

{T=t0}S{T<t0}例6：用加法實(shí)現(xiàn)乘法

{P:x>0y>0}z:=0;u:=x;repeatz:=z+y;u:=u-1;untilu=0{R:z=x*y}ρ:x*y=z+u*yu>0Q:x*y=z+u*yu>=0證明：1.{P}z:=0;u:=x;{P’}{P}z:=0;{x>0y>0z=0}u:=x;{x>0y>0z=0u=x}{P’}{x>0y>0z=0u=x}2.{P’}repeatz:=z+y;u:=u-1;untilu=0{R}1)

P’ρ顯然，{x>0y>0z=0u=x}{x*y=z+u*yu>0}成立。2){ρ}z:=z+y;u:=u-1;{Q}

{x*y=z+u*yu>0}z:=z+y;{x*y=z-y+u*yu>0}u:=u-1;{x*y=z+y+(u-1)*yu>-1}{x*y=z+u*yu>-1}{Q}3){QB}{ρ}{x*y=z+u*yu>=0u<>0}{x*y=z+u*yu>0}4){QB}{R}{x*y=z+u*yu>=0u=0}{x*y=zu=0}{x*y=z}{R}5){ρB}T>0{ρB}{x*y=z+u*yu>0u<>0}}因?yàn)門=u>0,所以{ρB}T>0成立6){T=t0}z:=z+y;u:=u-1;{T<t0}{u=t0}z:=z+y;{u=t0}u:=u-1;{u=t0-1<t0}{u=t0}{u<t0+1}z:=z+y;{u-1<t0}u:=u-1;{u<t0}

ρ:x*y=z+u*y∧u>0Q:x*y=z+u*y∧u>=01.

Pρ2.

{ρ}S{Q}3.

{QB}{ρ}4.

{QB}{R}5.

{ρB}T>06.

{T=t0}S{T<t0}3)forV:=AtoBdoS

分析：{P}forV:=AtoBdoS{Q}

第一次循環(huán)：{PV=A}S{Q(A)}

以后各次循環(huán)：當(dāng)V=Vi執(zhí)行S以后的后置斷言為Q(Vi){Q(predV)}S{Q(V)}Q(B)=Q,Q(B)Q(1)

A>B{P}={Q}(2)

A<=B則證明分析過程每步成立(3)

不需證明終止性，因?yàn)镕OR語句一定會(huì)終止的。{給定數(shù)組X,Y}begins:=0;{P:給定數(shù)組X,Ys=0}forI=1toNdoS:=S+X[I]*Y[I]end{Q:S=}證明：(1)

N<1{P:給定數(shù)組X,Ys=0}{Q:S=}所以，N<1是語句成立(2)

N>=1a)

{PI=1}S{Q(1)}{S=0I=1}S:=S+X[I]*Y[I]{S=}b)

{Q(pred(I))}S{Q(I)},{Q(I-1)}S{Q(I)}{S=}S:=S+X[I]*Y[I]{S=+X[I]*Y[I]}{S=}C)Q(B)=Q,Q(B)Q要證Q(B)=Q(N)=Q,即I=N,Q(N)==Q定義：假定S是一個(gè)語句，R是一個(gè)謂詞，它描述S執(zhí)行后所確定的某種關(guān)系。從S和R定義另外一個(gè)謂詞，記為wp(“S”,R),它表示：

“所有這樣的狀態(tài)的集合，S從其中任一狀態(tài)開始執(zhí)行必將在有限的時(shí)間內(nèi)終止于滿足R的狀態(tài)”。稱wp(“S”,R)是語句S關(guān)于R的最弱前置謂詞

-----------------S---------------終止{wp(“S”,R)}{R}一些狀態(tài)集合后置條件三、Dijkstra最弱前置條件方法

（二）最弱前置謂詞的幾個(gè)性質(zhì)公理

1、排奇律：wp(“S”,F)=F

要從某個(gè)狀態(tài)集的任何一個(gè)狀態(tài)出發(fā)執(zhí)行S后必定會(huì)終止，終止時(shí)滿足F，即使F為真，這樣的狀態(tài)是找不到的，因此對(duì)應(yīng)的狀態(tài)集為空。

2、合取分配律：wp(“S”,Q)wp(“S”,R)=wp(“S”,QR)表示從某一狀態(tài)開始執(zhí)行S，能終止，且分別滿足Ｑ和Ｒ的狀態(tài)，那它當(dāng)然也能終止，且滿足Ｑ∧Ｒ的狀態(tài)，反之亦然。

3、單調(diào)律：如果QR，則wp(“S”,Q)wp(“S”,R)4、折取分配律：wp(“S”,Q)wp(“S”,R)wp(“S”,QR)確定程序：從某一個(gè)狀態(tài)出發(fā)，程序不管執(zhí)行多少次，所經(jīng)過的路徑相同，所得的結(jié)果也相同。wp(“S”,Q)∨

wp(“S”,R)=wp(“S”,Q∨R)不確定程序：從某一個(gè)狀態(tài)出發(fā)，程序的任何兩次執(zhí)行可能得到的結(jié)果都不同，有時(shí)即便所得的結(jié)果相同，可能經(jīng)過的路徑也不同。wp(“S”,Q)∨

wp(“S”,R)

wp(“S”,Q∨R)

例：拋硬幣具有不確定性wp(“拋硬幣”，正面)=Fwp(“拋硬幣”，反面)=Fwp(“拋硬幣”，正面反面)=T

（三）求解最弱前置謂詞的規(guī)則

1、skip、abort、復(fù)合語句wp(“skip”,R)=R(相當(dāng)于空語句)wp(“abort”,R)=F(執(zhí)行過程中夭折的語句)wp(“S1,S2”,R)=wp(“S1”,wp(“S2”,R))（相當(dāng)于順序復(fù)合語句）例如wp(“skip;skip”,R)=wp(“skip”,wp(“skip”,R))=R2、賦值語句(1)單個(gè)簡單變量的賦值語句(2)多個(gè)簡單變量的賦值語句(3)單個(gè)數(shù)組元素的賦值（1）單個(gè)簡單變量的賦值語句

S::=I:=E其語義為：

wp(“I:=E”,R)=domain(E)canddomain(E)表示能獲得正常表達(dá)式E結(jié)果條件。

當(dāng)條件顯然時(shí)，可略去此項(xiàng)。表示表達(dá)式E去替換R中所有自由出現(xiàn)的變量I。B1candB2表示從左到右的次序計(jì)算，B1為F時(shí)，則不必計(jì)算B2,其結(jié)果全為F。B1為T時(shí)，則其結(jié)果為B2的結(jié)果。B1無定義時(shí)，其結(jié)果也無定義。1.wp(“x:=x+1”,x<0)=(x+1<0)=x<-12.wp(“x:=5”,x=5)=5=5=T3.wp(“x:=5”,x≠5)=5≠5=F4.wp(“x:=A÷B”,P(x))=(B≠0)candP(A÷B)5.wp(“x:=x*x”,x4=10)=((x*x)4=10)=x8=106.設(shè)數(shù)組B的下標(biāo)域?yàn)?：100，則:wp(“x:=B[I]”,x=B[I])=(0<=I<=100)candB[I]=B[I]=0<=I<=100練習(xí)7：wp(“t:=x;x:=y;y:=t”,x=X∧y=Y)=wp(“t:=x;x:=y”,wp(“y:=t”,x=X∧y=Y))=wp(“t:=x;x:=y”,x=X∧t=Y)=wp(“t:=x”,wp(“x:=y”,x=X∧t=Y))=wp(“t:=x”,y=X∧t=Y)=y=X∧x=Y(2)多個(gè)簡單變量的賦值語句8.wp(“x,y:=x-y,y-x,”,x+y=c)=(x-y+y-x=c)=0=c9.wp(“s,i:=s+b[i],i+1”,i>0^s=(∑j:0<=j<i:b[j]))=i+1>0^s+b[i]=(∑j:0<=j<i+1:b[j])=i>=0^s=(∑j:0<=j<i:b[j])10.{T}a:=a+1;b:=x{a=b}wp(“a:=a+1;b:=x”,a=b)=wp(“a:=a+1”,a=x)=a+1=x11.wp(“a:=a+1;b:=x(a,b)”,a=b)=wp(“a:=a+1”,a=x(a,b))=a+1=x(a+1,b)練習(xí)(3)單個(gè)數(shù)組元素的賦值語句對(duì)一個(gè)數(shù)組元素的賦值語句S::=b[i]:=E其中b是數(shù)組名，i是b的下標(biāo)表達(dá)式我們用（b;i:E)表示一個(gè)數(shù)組函數(shù)，定義為：(b;i:E)[j]=E當(dāng)i=jb[j]當(dāng)i≠j這樣，語句b[i]:=E等價(jià)于b:=(b;i:E)若略去domain(E)與domain(i)等因素，數(shù)組的賦值語句語義是wp(“b[i]:=E”,R)=Rb(b;i:E)其中Rb(b;i:E)表示用數(shù)組(b;i;E)去替換R中自由出現(xiàn)的數(shù)組名b練習(xí)12.wp(“b[i]:=5”,b[i]=5)=(b[i]=5)b(b;i:5)定義=(b;i:5)[i]=5替換=5=5=T13.wp(“b[i]:=5”,b[i]=b[j])=(b[i]=b[j])b(b;i:5)定義=(b;i:5)[i]=(b;i:5)[j]替換=(i≠j^5=b[j])∨(i=j^5=5)=(i≠j^5=b[j])∨(i=j)=(i≠j∨i=j)^(5=b[j]∨i=j)=T^(i=j∨b[j]=5)=i=j∨b[j]=514.wp(“b[b[i]]:=i”,b[i]=i)=(b[i]=i)b(b;b[i]:i)

(定義)=(b;b[i]:i)[i]=i(替換)=(b[i]≠i∧b[i]=i)∨(b[i]=i∧i=i)=F∨(b[i]=i∧T)=b[i]=i3、條件語句條件語句是任何一種高級(jí)語言中不可缺少的語句之一，常用if表示。大家已熟知，它一般有二種格式，即：

ifx≥0thenZ:=xelseZ:=-x

ifx<0thenZ:=-x為說明方便，我們可改寫成

ifx≥0→Z:=x

□x<0→Z:=―xfi與ifx≥0→skip□x<