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

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

2、 和和Q是斷言是斷言需要介紹斷言及推理規(guī)則需要介紹斷言及推理規(guī)則 P C Q 稱為程序規(guī)范稱為程序規(guī)范需要介紹規(guī)范語(yǔ)言及推理規(guī)則需要介紹規(guī)范語(yǔ)言及推理規(guī)則 Hoare邏輯也稱為語(yǔ)言的一種公理語(yǔ)義邏輯也稱為語(yǔ)言的一種公理語(yǔ)義作為例子的核心編程語(yǔ)言作為例子的核心編程語(yǔ)言 語(yǔ)法語(yǔ)法 整數(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邏輯邏輯 斷言語(yǔ)言斷言語(yǔ)言 用來(lái)描述程序變量滿足的性質(zhì)，如用來(lái)描述程序變量滿足的性質(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/一個(gè)簡(jiǎn)單的例子一個(gè)簡(jiǎ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 這些斷言形成一個(gè)格這些斷言形成一個(gè)格 變成計(jì)算變成計(jì)算WP(C, Q)并且證明并且證明P WP(C, Q)falsetrue強(qiáng)強(qiáng)弱弱Pre(C, Q)最弱前條件最弱前條件WP(C, Q)P最弱前條件演算最弱前條件演算 斷言形成一個(gè)格斷言形成一個(gè)格 WP(C, Q) = lub(Pre(C, Q) 按上面的式子計(jì)算按上面的式子計(jì)算WP(C, Q)有時(shí)是困難的有時(shí)是困難的1、lub P1, P2 = P1 P22、lub PS = P PS P3、但是當(dāng)集合、但是當(dāng)集合PS無(wú)限時(shí)怎么辦？無(wú)限時(shí)怎么辦？最弱前條件演算最弱前條件演算

8、斷言形成一個(gè)格斷言形成一個(gè)格 WP(C, Q) = lub(Pre(C, Q) 按上面的式子計(jì)算按上面的式子計(jì)算WP(C, Q)有時(shí)是困難的有時(shí)是困難的1、lub P1, P2 = P1 P22、lub PS = P PS P3、但是當(dāng)集合、但是當(dāng)集合PS無(wú)限時(shí)怎么辦？無(wú)限時(shí)怎么辦？ 即使得到了即使得到了WP(C, Q)，檢查蘊(yùn)涵，檢查蘊(yùn)涵P WP(C, Q)也可能是困難的也可能是困難的最弱前條件演算最弱前條件演算 演算規(guī)則（和演算規(guī)則（和Hoare邏輯規(guī)則對(duì)比）邏輯規(guī)則對(duì)比） 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ī)則 對(duì)于循環(huán)語(yǔ)句怎么辦？對(duì)于循環(huán)語(yǔ)句怎么辦？ 定義一族定義一族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ī)則 計(jì)算非常困難計(jì)算非常困難 能否找到容易一些并且夠用的辦法能否找到容易一些并且夠用的辦法 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)造一個(gè)驗(yàn)證條件我們構(gòu)造一個(gè)驗(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)的不變式是什么？?jī)H考慮內(nèi)存安全，外循環(huán)的不變式是什么？ 循環(huán)不變式的自動(dòng)生成是尚未解決的問(wèn)題循環(huán)不變式的自動(dòng)生成是尚未解決的問(wèn)題驗(yàn)證條件生成驗(yàn)證條件生成 驗(yàn)證條件生成驗(yàn)證條件生成 VC的計(jì)算

13、方式類似于的計(jì)算方式類似于WP的計(jì)算的計(jì)算 只有只有while語(yǔ)句例外語(yǔ)句例外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)終止時(shí)成立止時(shí)成立驗(yàn)證條件生成驗(yàn)證條件生成function mult(m, n) x = 0 ; y = 0 ;while y n do x = x + m ;y = y + 1 ; 以這個(gè)函數(shù)為以這個(gè)函數(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/ 第一個(gè)驗(yàn)證條件第一個(gè)驗(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 ; / 在語(yǔ)句序列中的斷言在語(yǔ)句序列中的斷言 (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個(gè)驗(yàn)證條件個(gè)驗(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 +