第7章程序驗證(編輯修改稿)
2024-10-07 09:06 本頁面
【文章內容簡介】 E, Q) = Q[E/x] – WP(C1。C2 , Q) = WP (C1, WP(C2, Q)) – WP(if B {C1} else {C2}, Q) = (B ? WP(C1, Q)) ? (?B ? WP(C2, Q)) { Q[E/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ī)則 – 對于循環(huán)語句怎么辦？ – 定義一族 WP – WPk(while B { C }, Q) = “ 循環(huán)的執(zhí)行終止于不多于 k次的迭代，其終止狀態(tài)滿足 Q” 的最弱前條件： – WP0 = ? B ? Q – WP1 = B ? WP(C, WP0) ? ? B ? Q . . . – WP(while B {C}, Q) = ?k? 0WPk = lub{WPk | k ? 0} { I ? B } C { I } { I } while B {C } { Q } 最弱前條件演算 ? 演算規(guī)則 – 計算非常困難 – 能否找到容易一些并且夠用的辦法 – WPk(while B { C }, Q) = “ 循環(huán)的執(zhí)行終止于不多于 k次的迭代，其終止狀態(tài)滿足 Q” 的最弱前條件： – WP0 = ? B ? Q – WP1 = B ? WP(C, WP0) ? ? B ? Q . . . – WP(while B {C}, Q) = ?k? 0WPk = lub{WPk | k ? 0} 驗證條件生成 ? 驗證條件 – 回想一下我們想達到的目的 false true ? 強 弱 Pre(C, Q) P 最弱前條件 WP(C, Q) 驗證條件生成 ? 驗證條件 – 回想一下我們想達到的目的 – 我們構造一個驗證條件 VC(C, Q) 循環(huán)需要有循環(huán)不變式標注 VC要強于 WP 但仍然要弱于 P， P ? VC(C, Q) ? WP(C, Q) false true ? 強 弱 Pre(C, Q) 最弱前條件 WP(C, Q) P 驗證條件 VC(C, Q) 驗證條件生成 ? 驗證條件 – 循環(huán)不變式很難寫出 , 考慮源于 QuickSort的代碼 int partition(int *a, int L0, int H0, int pivot) { int L = L0, H = H0。 while(L H) { while(a[L] pivot) L++。 while(a[H] pivot) H 。 if(L H) { swap a[L] and a[H] } } return L } // 僅考慮內存安全，外循環(huán)的不變式是什么？ – 循環(huán)不變式的自動生成是尚未解決的問題 驗證條件生成 ? 驗證條件生成 – VC的計算方式類似于 WP的計算 – 只有 while語句例外 VC(while B {C }, Q ) = I ? ( I ? B ? VC(C, I) ) ? (?I ? B ? Q ) – 循環(huán)
教學課件相關推薦
鄂ICP備17016276號-1