【文章內(nèi)容簡介】 Q[E/x]} x = E {Q} – WP(S1。S2, Q) = WP (S1, WP(S2, Q)) – WP(if E then S1 else S2, Q) = (WP(S1, Q) ? E) ? (WP(S2, Q) ? ?E) {P} S1 {R} {R} S2 {Q} {P} S1。 S2 {Q} {P ? E} S1 {Q} {P ? ?E} S2 {Q} {P } if E then S1 else S2 {Q} 26 生成驗證條件的演算 ? 最弱前條件演算 WP – 對于 WP (while E do S, Q)，演算有可能不終止 假定 WPk為循環(huán)體 S執(zhí)行 k次的演算 WP0(while E do S, Q) = ?E ? Q WPi (while E do S, Q) = E ? WP(S, WPi?1(while E do S, Q)) WP(while E do S, Q) = WP0 (…) ? WP1 (…) ? WP2 (…) ? … {I?E} S {I} {I} while E do S {I??E} WP演算在循環(huán)語句 這里遇到了困難 27 生成驗證條件的演算 ? 最弱前條件演算 WP – 一些其他規(guī)則 (1) WP(S, Q1 ? Q2) = WP(S, Q1) ? WP(S, Q2) (2) WP(S, Q1 ? Q2) = WP(S, Q1) ? WP(S, Q2) (3) (4) WP(S, false) = false (4)和 (5)較難理解 , 不介紹 (5) WP(S, true) = 保證 S終止的最弱前條件 … … …. – 下面考慮解決由循環(huán)語句引出的問題 Q ? Q? WP(S, Q) ? WP(S, Q?) 28 生成驗證條件的演算 ? 生成驗證條件的演算 VC(verification condition) (1) 觀察 P和 WP之間的關系 (2) 尋找兩者之間的一種稱為 VC(S, Q)的演算 (3) 即 P ?VC(S, Q)?WP(S, Q) (4) VC演算的特點：要求驗證者提供循環(huán)不變式 false true ? strong weak Precondition(S, Q) 最弱前條件 WP(S, Q) 驗證者提供的前條件 P 驗證條件演算結果 VC(S, Q) 29 生成驗證條件的演算 ? 生成驗證條件的演算 VC(verification condition) – 除了循環(huán)語句外， VC演算與 WP的一致 – 循環(huán)語句的 VC演算如下，其中 I是循環(huán)不變式 VC(while E do S, Q) = I ? ?x1…x n(( I ? E ? VC(S, I)) ? (I ? ?E ? Q)) 其中 x1, …, x n是在 S中被修改的所有變量 – 實際做法 (1) 黃色部分和綠色部分 分別作為循環(huán)出口和入口的驗證條件 (2) I作為繼續(xù)逆向 VC演算的后斷言 {I?E} S {I} {I} while E do S {I??E} 30 程 序 驗 證 實 例 void mult(int m, int n) { x = 0 。 y = 0 。 while (y n) do { x = x + m 。 y = y + 1 。 } } 例子：用加運算來實現(xiàn)乘運算的函數(shù) 31 程 序 驗 證 實 例 n ? 0 // 前條件 void mult(int m, int n) { x = 0 。 y = 0 。 while (y n) do { x = x + m 。 y = y + 1 。 } } x == m ? n // 后條件 由程序員提供 由程序員提供 32 程 序 驗 證 實 例 n ? 0 void mult(int m, int n) { x = 0 。 y = 0 。 while (y n) do { (x == m?y) ? (y ? n) // 循環(huán)不變式 x = x + m 。 y = y + 1 。 } } x == m ? n 也由程序員提供 33 程 序 驗 證 實 例 n ? 0 void mult(int m, int n) { x = 0 。 y = 0 。 while (y n) do { (x == m?y) ? (y ? n) // 循環(huán)不變式 x = x + m 。 y = y + 1 。 } } x == m ? n 函數(shù)前后條件、循環(huán)不變式 都稱為斷言 它們看上去像編程語言的布 爾表達式 34 程 序 驗 證 實 例 n ? 0 void mult(int m, int n) { x = 0 。 y = 0 。 while (y n) do { (x == m?y) ? (y ? n) x = x + m 。 y = y + 1 。 } ((x == m?y) ? (y ? n)) ? ?(y n) // 循環(huán)結束程序點的斷言 } x == m ? n I ? ?E 35 程 序 驗 證 實 例 n ? 0 void mult(int m, int n) { x = 0 。 y = 0 。 while (y n) do { (x == m?y) ? (y ? n) x = x + m 。 y = y + 1 。 } ((x == m?y) ? (y ? n)) ? ?(y n) ? (x == m?n) } x == m ? n I ? ?E ? Q（ Q是函數(shù)后條件） 第 1個驗證條件 36 程 序 驗 證 實 例 n ? 0 void mult(int m, int 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) ((x == m?y) ? (y ? n)) ? ?(y n) ? (x == m?n) } x == m ? n 通過最弱前條件演算得到 37 程 序 驗 證 實 例 n ? 0 void mult(int m, int n) { x = 0 。 y = 0 。 while (y n) do { (x == m?y) ? (y ? n) (x+m == m?(y+1)) ? ((y+1) ?