程序验证
第7章程序验证(编辑修改稿)
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