第7章程序驗證(文件)
【正文】 言形成一個格 WP(C, Q) = lub?(Pre(C, Q)) – 按上面的式子計算 WP(C, Q)有時是困難的 lub {P1, P2} = P1 ? P2 lub PS = ?P?PS P 但是當(dāng)集合 PS無限時怎么辦？ – 即使得到了 WP(C, Q)，檢查蘊涵 P ? WP(C, Q)也可能是困難的 最弱前條件演算 ? 演算規(guī)則（和 Hoare邏輯規(guī)則對比） – WP(x = E, Q) = Q[E/x] – WP(C1。 while(a[H] pivot) H 。 y = y + 1 。 y = y + 1 。 y = y + 1 。 y = y + 1 。 (x = m?(y+1)) ? ((y+1) ? n) y = y + 1 。 (x = m?(y+1)) ? ((y+1) ? n) y = y + 1 。 (x = m?(y+1)) ? ((y+1) ? n) y = y + 1 。 (x = m?(y+1)) ? ((y+1) ? n) y = y + 1 。 (x = m?(y+1)) ? ((y+1) ? n) y = y + 1 。 (x = m?(y+1)) ? ((y+1) ? n) y = y + 1 。 y = y + 1 。 y = 0 。 (x = m?0) ? (0 ? n) y = 0 。 (x = m?0) ? (0 ? n) y = 0 。 (x = m?0) ? (0 ? n) y = 0 。 y = 0 。 y = 0 。 y = 0 。 y = 0 。 y = 0 。 y = 0 。 y = 0 。 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次的迭代，其終止?fàn)顟B(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次的迭代，其終止?fàn)顟B(tài)滿足 Q” 的最弱前條件： – WP0 = ? B ? Q – WP1 = B ? WP(C, WP0) ? ? B ? Q . . . – WP(while B {C}, Q) = ?k? 0WPk = lub{WPk | k ? 0} 驗證條件生成 ? 驗證條件 – 回想一下我們想達(dá)到的目的 false true ? 強 弱 Pre(C, Q) P 最弱前條件 WP(C, Q) 驗證條件生成 ? 驗證條件 – 回想一下我們想達(dá)到的目的
教學(xué)課件相關(guān)推薦
鄂ICP備17016276號-1