第7章程序驗(yàn)證

1、第第7章章 程序驗(yàn)證程序驗(yàn)證內(nèi)容概述內(nèi)容概述 程序邏輯：描述和論證程序行為的邏輯程序邏輯：描述和論證程序行為的邏輯 Hoare邏輯邏輯 Dijkstra最弱前條件演算最弱前條件演算 從程序到定理從程序到定理 驗(yàn)證條件生成驗(yàn)證條件生成 從定理到證明從定理到證明 定理證明器定理證明器 判定過程判定過程 循環(huán)不變式的推斷循環(huán)不變式的推斷 以以George C. Necula教授的講稿為主來介紹教授的講稿為主來介紹程程 序序 邏邏 輯輯 Hoare邏輯邏輯 良形公式良形公式（well-formed formula）的形式為的形式為 P C Q C是程序片段是程序片段需要介紹編程語言需要介紹編程語言 P

2、 和和Q是斷言是斷言需要介紹斷言及推理規(guī)則需要介紹斷言及推理規(guī)則 P C Q 稱為程序規(guī)范稱為程序規(guī)范需要介紹規(guī)范語言及推理規(guī)則需要介紹規(guī)范語言及推理規(guī)則 Hoare邏輯也稱為語言的一種公理語義邏輯也稱為語言的一種公理語義作為例子的核心編程語言作為例子的核心編程語言 語法語法 整數(shù)表達(dá)式整數(shù)表達(dá)式E := n | x | E | E + E | E E | E E | ( E ) 布爾表達(dá)式布爾表達(dá)式B := true | false | !B | B & B | B | B | E E | ( B ) 命令命令C := x = E | C ; C | if B C else C |w

3、hile B C 例子例子y = 1; z = 0; while (z != x) z = z +1; y = y z Hoare邏輯邏輯 斷言語言斷言語言 用來描述程序變量滿足的性質(zhì)，如用來描述程序變量滿足的性質(zhì)，如x=5, x+y = 0 a = x + 1;y = 1;if (a -1 = 0 ) z = 0;y = 1;while ( z != x ) else z = z + 1;y = a;y = y z; y = x + 1 y = x ! Hoare邏輯邏輯 例例2 Fac1 例例3 Fac2 x = 0 x0是輔助的邏輯變量是輔助的邏輯變量 y = 1; x = 0 x =

4、x0 z = 0; y = 1; while ( z != x ) while ( x != 0 ) z = z + 1; y = y x;y = y z; x = x 1; y = x ! y = x0 ! Hoare邏輯邏輯 部分正確性的證明規(guī)則部分正確性的證明規(guī)則 賦值公理賦值公理賦值公理的實(shí)例賦值公理的實(shí)例 2 = 2 x = 2 x = 2 2 = 4 x = 2 x = 4 2 = y x = 2 x = y 2 0 x = 2 x 0 x + 1 + 5 = y x = x + 1 x + 5 =y x + 1 0 y 0 x = x + 1 x 0 y 0 QE/x x = E

5、 Q Hoare邏輯邏輯 部分正確性的證明規(guī)則部分正確性的證明規(guī)則 賦值公理賦值公理 復(fù)合規(guī)則復(fù)合規(guī)則 條件規(guī)則條件規(guī)則 循環(huán)規(guī)則循環(huán)規(guī)則 QE/x x = E Q P C1 R R C2 Q P C1; C2 Q P B C1 Q P B C2 Q P if B C1 else C2 Q I B C I I while B C I B Hoare邏輯邏輯 部分正確性的證明規(guī)則部分正確性的證明規(guī)則 推論規(guī)則推論規(guī)則AR P P 表示表示P P在謂詞邏輯的自然演繹演在謂詞邏輯的自然演繹演算中可以證明算中可以證明 AR P P P C Q AR Q Q P C Q Hoare邏輯邏輯n = 0fu

6、nction mult(m, n) (0 = m 0) (0 = n) x = 0 ; (x = m 0) (0 = n) y = 0 ; (x = m y) (y = n) while y n do (x+m = m (y+1) (y+1) = n) x = x + m ; (x = m (y+1) (y+1) = n) y = y + 1 ; (x = m y) (y = n) x = m n/一個簡單的例子一個簡單的例子最弱前條件演算最弱前條件演算 Dijkstra的思路的思路 為了驗(yàn)證為了驗(yàn)證 P C Q ，找出所有使得，找出所有使得 P C Q 的斷言的斷言P ，稱為，稱為Pre(C

7、, Q) 驗(yàn)證存在驗(yàn)證存在P Pre(C, Q) that P P 這些斷言形成一個格這些斷言形成一個格 變成計算變成計算WP(C, Q)并且證明并且證明P WP(C, Q)falsetrue強(qiáng)強(qiáng)弱弱Pre(C, Q)最弱前條件最弱前條件WP(C, Q)P最弱前條件演算最弱前條件演算 斷言形成一個格斷言形成一個格 WP(C, Q) = lub(Pre(C, Q) 按上面的式子計算按上面的式子計算WP(C, Q)有時是困難的有時是困難的1、lub P1, P2 = P1 P22、lub PS = P PS P3、但是當(dāng)集合、但是當(dāng)集合PS無限時怎么辦？無限時怎么辦？最弱前條件演算最弱前條件演算

8、斷言形成一個格斷言形成一個格 WP(C, Q) = lub(Pre(C, Q) 按上面的式子計算按上面的式子計算WP(C, Q)有時是困難的有時是困難的1、lub P1, P2 = P1 P22、lub PS = P PS P3、但是當(dāng)集合、但是當(dāng)集合PS無限時怎么辦？無限時怎么辦？ 即使得到了即使得到了WP(C, Q)，檢查蘊(yùn)涵，檢查蘊(yùn)涵P WP(C, Q)也可能是困難的也可能是困難的最弱前條件演算最弱前條件演算 演算規(guī)則（和演算規(guī)則（和Hoare邏輯規(guī)則對比）邏輯規(guī)則對比） WP(x = E, Q) = QE/x WP(C1;C2 , Q) = WP (C1, WP(C2, Q) WP(i

9、f B C1 else C2, Q) = (B WP(C1, Q) ( B WP(C2, Q) QE/x x = E Q P C1 R R C2 Q P C1; C2 Q P B C1 Q P B C2 Q P if B C1 else C2 Q 最弱前條件演算最弱前條件演算 演算規(guī)則演算規(guī)則 對于循環(huán)語句怎么辦？對于循環(huán)語句怎么辦？ 定義一族定義一族WP WPk(while B C , Q) = “循環(huán)的執(zhí)行終止于不循環(huán)的執(zhí)行終止于不多于多于k次的迭代，其終止?fàn)顟B(tài)滿足次的迭代，其終止?fàn)顟B(tài)滿足Q”的最弱前的最弱前條件：條件： WP0 = B Q WP1 = B WP(C, WP0) B Q.

10、. . WP(while B C, Q) = k 0WPk = lubWPk | k 0 I B C I I while B C Q 最弱前條件演算最弱前條件演算 演算規(guī)則演算規(guī)則 計算非常困難計算非常困難 能否找到容易一些并且夠用的辦法能否找到容易一些并且夠用的辦法 WPk(while B C , Q) = “循環(huán)的執(zhí)行終止于不循環(huán)的執(zhí)行終止于不多于多于k次的迭代，其終止?fàn)顟B(tài)滿足次的迭代，其終止?fàn)顟B(tài)滿足Q”的最弱前的最弱前條件：條件： WP0 = B Q WP1 = B WP(C, WP0) B Q. . . WP(while B C, Q) = k 0WPk = lubWPk | k 0驗(yàn)

11、證條件生成驗(yàn)證條件生成 驗(yàn)證條件驗(yàn)證條件 回想一下我們想達(dá)到的目的回想一下我們想達(dá)到的目的falsetrue強(qiáng)強(qiáng)弱弱Pre(C, Q)P最弱前條件最弱前條件WP(C, Q)驗(yàn)證條件生成驗(yàn)證條件生成 驗(yàn)證條件驗(yàn)證條件 回想一下我們想達(dá)到的目的回想一下我們想達(dá)到的目的 我們構(gòu)造一個驗(yàn)證條件我們構(gòu)造一個驗(yàn)證條件VC(C, Q)1、循環(huán)需要有循環(huán)不變式標(biāo)注、循環(huán)需要有循環(huán)不變式標(biāo)注2、VC要強(qiáng)于要強(qiáng)于WP3、但仍然要弱于、但仍然要弱于P， P VC(C, Q) WP(C, Q)falsetrue強(qiáng)強(qiáng)弱弱Pre(C, Q)最弱前條件最弱前條件WP(C, Q)P驗(yàn)證條件驗(yàn)證條件VC(C, Q)驗(yàn)證條件生成

12、驗(yàn)證條件生成 驗(yàn)證條件驗(yàn)證條件 循環(huán)不變式很難寫出循環(huán)不變式很難寫出, 考慮源于考慮源于QuickSort的代碼的代碼int partition(int *a, int L0, int H0, int pivot) int L = L0, H = H0; while(L H) while(aL pivot) H -; if(L H) swap aL and aH return L / 僅考慮內(nèi)存安全，外循環(huán)的不變式是什么？僅考慮內(nèi)存安全，外循環(huán)的不變式是什么？ 循環(huán)不變式的自動生成是尚未解決的問題循環(huán)不變式的自動生成是尚未解決的問題驗(yàn)證條件生成驗(yàn)證條件生成 驗(yàn)證條件生成驗(yàn)證條件生成 VC的計算

13、方式類似于的計算方式類似于WP的計算的計算 只有只有while語句例外語句例外VC(while B C , Q ) = I ( I B VC(C, I) ) ( I B Q ) 循環(huán)不變式循環(huán)不變式 I 由外部提供由外部提供 I B C I I while B C Q I 在循環(huán)在循環(huán)入口成立入口成立I 在循環(huán)任意在循環(huán)任意次迭代都保持次迭代都保持Q 在循環(huán)終在循環(huán)終止時成立止時成立驗(yàn)證條件生成驗(yàn)證條件生成function mult(m, n) x = 0 ; y = 0 ;while y n do x = x + m ;y = y + 1 ; 以這個函數(shù)為以這個函數(shù)為例，解釋驗(yàn)證例，解釋驗(yàn)證

14、條件生成條件生成驗(yàn)證條件生成驗(yàn)證條件生成n 0/ 前條件前條件function mult(m, n) x = 0 ; y = 0 ;while y n do x = x + m ;y = y + 1 ; x = m n/ 后條件后條件驗(yàn)證條件生成驗(yàn)證條件生成n 0function mult(m, n) x = 0 ; y = 0 ;while y n do (x = m y) (y n) / 循環(huán)不變式循環(huán)不變式x = x + m ;y = y + 1 ; x = m n驗(yàn)證條件生成驗(yàn)證條件生成n 0function mult(m, n) x = 0 ; y = 0 ;while y n do

15、 (x = m y) (y n) x = x + m ;y = y + 1 ; (x = m y) (y n) (y n) (x = m n) x = m n/ 第一個驗(yàn)證條件第一個驗(yàn)證條件由驗(yàn)證條件由驗(yàn)證條件生成器生成生成器生成驗(yàn)證條件生成驗(yàn)證條件生成n 0function mult(m, n) x = 0 ; y = 0 ;while y n do (x = m y) (y n) x = x + m ;(x = m (y+1) (y+1) n)y = y + 1 ; / 在語句序列中的斷言在語句序列中的斷言 (x = m y) (y n) (y n) (x = m n) x = m n由最

16、弱前條由最弱前條件演算插入件演算插入驗(yàn)證條件生成驗(yàn)證條件生成n 0function mult(m, n) x = 0 ; y = 0 ;while y n do (x = m y) (y n) (x+m = m (y+1) (y+1) n) x = x + m ;(x = m (y+1) (y+1) n) y = y + 1 ; (x = m y) (y n) (y n) (x = m n) x = m n驗(yàn)證條件生成驗(yàn)證條件生成n 0function mult(m, n) x = 0 ; y = 0 ;(x = m y) (y n) (y n) (x+m = m (y+1) (y+1) n)

17、while y n do (x = m y) (y n) (x+m = m (y+1) (y+1) n) x = x + m ;(x = m (y+1) (y+1) n) y = y + 1 ; (x = m y) (y n) (y n) (x = m n) x = m n第第2個驗(yàn)證條件個驗(yàn)證條件驗(yàn)證條件生成驗(yàn)證條件生成n 0function mult(m, n) x = 0 ;(x = m 0) (0 n) y = 0 ;(x = m y) (y n) (y n) (x+m = m (y+1) (y+1) n)while y n do (x = m y) (y n) (x+m = m (y

18、+1) (y+1) n) x = x + m ;(x = m (y+1) (y+1) n) y = y + 1 ; (x = m y) (y n) (y n) (x = m n) x = m n驗(yàn)證條件生成驗(yàn)證條件生成n 0function mult(m, n)(0 = m 0) (0 n) x = 0 ;(x = m 0) (0 n) y = 0 ;(x = m y) (y n) (y n) (x+m = m (y+1) (y+1) n)while y n do (x = m y) (y n) (x+m = m (y+1) (y+1) n) x = x + m ;(x = m (y+1) (y+1) n) y = y + 1 ; (x = m y) (y n) (y n) (x = m n) x = m n驗(yàn)證條件生成驗(yàn)證條件生成n 0function mult(m, n) ( n 0 ) (0 = m 0) (0 n)(0 = m 0) (0 n) x = 0 ;(x = m 0) (0 n) y = 0 ;(x = m y) (y n) (y n) (x+m = m (y+1) (y+1) n)while y n do (x = m y) (y n) (x+m = m (y+1) (y+1) n) x = x +