程序的公理化證明

1、程序的公理化證明趙建華南京大學計算機系簡介 C.A.R. Hoare提出的公理系統(tǒng) 斷言中包含了邏輯公式和代碼 組合式證明 先證明程序的各個部分，然后把這些證明組合起來，得到更大代碼的證明。 本證明系統(tǒng)基于某個一階推理系統(tǒng).斷言的形式 Hoare三元式P S Q S ：代碼 P(pre-condition，前置條件) Q (post-condition，后置條件) P和Q是一階邏輯公式 三元式指出了一個部分正確性 如果S從一個滿足P的狀態(tài)開始執(zhí)行，且S 能夠正常執(zhí)行完畢，那么最后的狀態(tài)滿足Q。程序的抽象語法 基本語句 賦值語句：v:=e skip語句 復合語句 順序：S;S 選擇：if p t

2、hen S else S fi 循環(huán)：while p do S公理：賦值語句Qe/v v:=e Q 如果語句v:=e執(zhí)行之前的狀態(tài)滿足 Qe/v，那么v:=e執(zhí)行之后的狀態(tài)滿足Q。Qe/v表示將公式Q中的v替換成為e后得到的公式。 例如：x+1=10 x:=x+1x=10公理：skip語句 skip語句不改變狀態(tài)。P skip Ppre,post規(guī)則 在證明了一個斷言之后，我們可以弱化其后置條件，或者強化其前置條件。P=P，P S QP S QP S Q，Q = QP S Q順序組合規(guī)則 在證明一個順序組合語句的時候，我們可以先分別證明兩個子語句的性質，然后將其合并得到整個組合語句的性質。P

3、S1 Q， QS2RP S1;S2 Rif-then-else規(guī)則Pp S1 Q ，Pp S2 Q P if p then S1 else S2 Q if語句的語義是：如果p成立，則執(zhí)行S1，否則執(zhí)行S2。 前提條件表明 如果開始狀態(tài)滿足Pp那么執(zhí)行了S1 之后滿足Q。 如果開始狀態(tài)滿足P p，那么執(zhí)行S之后仍然滿足Q。 如果開始狀態(tài)滿足P，那么它要么滿足Pp，要么滿足P p。從if語句的含義我們可以知道結論成立。while規(guī)則(部分正確性)Pp S PPwhile p do S P P被稱為while語句的不變式。 在while語句的執(zhí)行過程中，這個性質總是成立。 而while語句會執(zhí)行到p

4、不成立為止。 因此，當while語句退出循環(huán)時，狀態(tài)必然滿足Pp。 這個性質不保證whilewhile語句會退出循環(huán)while規(guī)則(完全正確性) 如果能夠找到一個函數(shù)f f的取值和變量取值有關，且 Pp f0 且對任意的常數(shù)f0，f=f0 S ff0, 那么循環(huán)必然終止 for(int i = 0; ix2 doy1:=y1+1;y2:=y2-x2end 要證明如下結論：當x1=0, x2=0成立時，最終得到的y1是x1/x2的整數(shù)商部分，y2是x1/x2的余數(shù)部分即：Precondition: x1=0 x2=0Postcondition：x1=y1*x2+y2 y2=0 y2=0 x20y1=0;x1=0 x20 y1=0y2=x1;x1=y1*x2+y2 y2=0while y2=x2 dox1=y1*x2+y2 y2=x2y1:=y1+1;x1=y1*x2+y2-x2 y2=x2 y2:=y2-x2x1=y1*x2+y2 y2=0 endx1=y1*x2+y2 y2=0 y2x2 練習 考慮輾轉相除法求解GCD的算法的正確性證明 考慮圖論中最短路徑的Floyd算法的正確性。Hoare Logic不能處理指針/數(shù)組 反例1： true mm2 := 3 mm2 = 3 當原來m2=2時， 賦值之后，m2等于3，mm2