Hoare逻辑 ·部分正确性的证明规则 -赋值公理 {2IE]}x=E{2 -复合规则 AP}CIRY {R}C2{2} {P}C1;C2{2} -条件规则 {PAB}C1{2}{P∧B}C2{2} {P}if B{C1}else {C2) -循环规则 {I∧B}C{I} {I}while B{C}{∧-ByHoare逻辑 • 部分正确性的证明规则 – 赋值公理 – 复合规则 – 条件规则 – 循环规则 { 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 } { I  B } C { I } { I } while B {C } {I  B}