【正文】 } ((x = m?y) ? (y ? n)) ? ?(y n) ? (x = m?n) } x = m ? n 驗證條件生成 n ? 0 function mult(m, n){ ( n ? 0 ) ? ((0 = m?0) ? (0 ? n)) (0 = m?0) ? (0 ? n) x = 0 。 // 在語句序列中的斷言 } ((x = m?y) ? (y ? n)) ? ?(y n) ? (x = m?n) } x = m ? n 由最弱前條件演算插入 驗證條件生成 n ? 0 function mult(m, n){ x = 0 。 } } 以這個函數(shù)為例，解釋驗證條件生成 驗證條件生成 n ? 0 // 前條件 function mult(m, n){ x = 0 。 y = y ? z。 z = 0。 y = a。 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) 驗證條件生成 ? 驗證條件 – 回想一下我們想達到的目的 – 我們構(gòu)造一個驗證條件 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。 y = 0 。 (x = m?0) ? (0 ? n) y = 0 。 y = y + 1 。 (x = m?(y+1)) ? ((y+1) ? n) y = y + 1 。 y = y + 1 。