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

1、程序的結構要簡單2、采用標準的軟件設計工具、標準的算法手冊以及有效的程序設計方法發現錯誤的方法

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

程序測試的過程…軟件測試方法軟件測試的方法和技術是多種多樣的。對于軟件測試技術，根據不同角度，可以將測試方法分為不同種類。（1）從是否需要執行被測軟件的角度，可以分為靜態測試和動態測試；（2）從測試是否針對系統內部結構和具體實現算法的角度，可以分為白盒測試和黑盒測試；（3）從實際測試的前后過程來看，軟件測試是由一系列的不同測試組成，這些步驟可以分為：單元測試、組裝測試（集成測試）、確認測試和系統測試。兩種重要的軟件測試方法

黑盒測試這種方法是把測試對象看做一個黑盒子，測試人員完全不考慮程序內部的邏輯結構和內部特性，只依據程序的需求規格說明書，檢查程序的功能是否符合它的功能說明。黑盒測試又叫做功能測試或數據驅動測試。

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

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

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

。測試常常是不充分的，它只能發現某些錯誤存在，而不能證明錯誤的不存在

?！诤袦y試

等價類劃分

邊界值分析

錯誤推測法

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

例如，在程序的規格說明中，對輸入條件有一句話：“……項數可以從1到999……”，則有效等價類是“1≤項數≤999”兩個無效等價類是“項數＜1”或“項數＞999”。在數軸上表示成:

邊界值分析

人們從長期的測試工作經驗得知，大量的錯誤是發生在輸入或輸出范圍的邊界上，而不是在輸入范圍的內部。因此針對各種邊界情況設計測試用例，可以查出更多的錯誤。比如，在做三角形計算時，要輸入三角形的三個邊長：A、B和C。我們應注意到這三個數值應當滿足

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

邏輯覆蓋：以程序內部的邏輯結構為基礎的設計測試用例的技術。

語句覆蓋

判定覆蓋

條件覆蓋

判定－條件覆蓋

條件組合覆蓋

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

以上這些數據雖然均達到一些測試目的，且各有側重，但是都是不充分的。如從條件出發，用組合的辦法使各個條件都能執行到，則我們可以寫出以下8種條件組合：1)A>1,B=02)A>1,B<>0;(<>是不等號)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滿足條件組合覆蓋必滿足判定、條件、判定/條件覆蓋，但仍不能遍歷每條路徑。根據這8種條件組合，又可以優化組成如下4組數據：A=2,B=0,X=4A=2,B=1,X=1A=1,B=0,X=2A=1,B=1,X=1它們都能使各種條件均能出現一次。雖然這個組合方法比較方便，邏輯也很清楚，且對執行條件來說還是比較全面的，但是仍然又未走遍的路徑，如acbd在測試時，還要注意到計算機執行多個條件的特點，即它必須把多個條件分解為簡單判別才能執行，如上述例子可分解為右圖。

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

測試用例通過ABX路徑

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

美國SEGUE公司的SILK系列自動測試技術。SILK系列自動化黑盒測試平臺能夠全面適應電子商務技術的最新發展，具有測試自動化，易用易維護，場景模擬精確，支持分布式測試，支持多標準協議，擴展性強等優點。

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

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

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

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

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

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

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

5)凡蘊含一語句前提的斷言，都是這個語句的前提。凡一語句結論所蘊含的斷言，都是這個語句的結論。

上述規則將作為工具，對程序進行驗證。

（二）簡單語句的證明

1、空語句

2、賦值語句

{P}{P}結論即為前提

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

來記，其中

是規則的前提，H是結論，它表示如果

為真，那么H也為真。

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

5、分情選擇語句

4、復合語句

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

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

，

D=2x-1，求順序執行下列各語句后的結論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}，求執行語句后的結論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：

計算X=MAX(A,B)的程序為ifA>=BthenX:=AelseX:=B試驗證其正確性。

證明：{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)}

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

ρ稱為循環不變式：一個在每次循環的前后均為真的謂詞。

終止性：

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

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

1.

Pρ2.

{ρB}S{ρ}3.

{ρB}{Q}4.

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

例5：

求兩個自然數相除所得的商（在Q中）和余數（在R中）

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

證明：(1)P={x>0y>0}Q:=0;R:=x;P1={x>0y>0Q=0R=x}(2)循環語句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：用加法實現乘法

{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}}因為T=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}

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

以后各次循環：當V=Vi執行S以后的后置斷言為Q(Vi){Q(predV)}S{Q(V)}Q(B)=Q,Q(B)Q(1)

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

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

不需證明終止性，因為FOR語句一定會終止的。{給定數組X,Y}begins:=0;{P:給定數組X,Ys=0}forI=1toNdoS:=S+X[I]*Y[I]end{Q:S=}證明：(1)

N<1{P:給定數組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是一個語句，R是一個謂詞，它描述S執行后所確定的某種關系。從S和R定義另外一個謂詞，記為wp(“S”,R),它表示：

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

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

（二）最弱前置謂詞的幾個性質公理

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

要從某個狀態集的任何一個狀態出發執行S后必定會終止，終止時滿足F，即使F為真，這樣的狀態是找不到的，因此對應的狀態集為空。

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

3、單調律：如果QR，則wp(“S”,Q)wp(“S”,R)4、折取分配律：wp(“S”,Q)wp(“S”,R)wp(“S”,QR)確定程序：從某一個狀態出發，程序不管執行多少次，所經過的路徑相同，所得的結果也相同。wp(“S”,Q)∨

wp(“S”,R)=wp(“S”,Q∨R)不確定程序：從某一個狀態出發，程序的任何兩次執行可能得到的結果都不同，有時即便所得的結果相同，可能經過的路徑也不同。wp(“S”,Q)∨

wp(“S”,R)

wp(“S”,Q∨R)

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

（三）求解最弱前置謂詞的規則

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

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

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

當條件顯然時，可略去此項。表示表達式E去替換R中所有自由出現的變量I。B1candB2表示從左到右的次序計算，B1為F時，則不必計算B2,其結果全為F。B1為T時，則其結果為B2的結果。B1無定義時，其結果也無定義。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.設數組B的下標域為0：100，則:wp(“x:=B[I]”,x=B[I])=(0<=I<=100)candB[I]=B[I]=0<=I<=100練習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)多個簡單變量的賦值語句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)練習(3)單個數組元素的賦值語句對一個數組元素的賦值語句S::=b[i]:=E其中b是數組名，i是b的下標表達式我們用（b;i:E)表示一個數組函數，定義為：(b;i:E)[j]=E當i=jb[j]當i≠j這樣，語句b[i]:=E等價于b:=(b;i:E)若略去domain(E)與domain(i)等因素，數組的賦值語句語義是wp(“b[i]:=E”,R)=Rb(b;i:E)其中Rb(b;i:E)表示用數組(b;i;E)去替換R中自由出現的數組名b練習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、條件語句條件語句是任何一種高級語言中不可缺少的語句之一，常用if表示。大家已熟知，它一般有二種格式，即：

ifx≥0thenZ:=xelseZ:=-x

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

ifx≥0→Z:=x

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