演绎规则的例子 规则前驱 后继 赋值:x=expr ( P(expr)x: expr(P(x) While:{P∧B}S{P} iPi while b do s end P A(not B) if--then--else B∧P}Sn{Q},{(notB)∧P}S2{Q} (P if b then Si else $ Q)演绎规则的例子 规则 前驱 后继 赋值：x:=expr {P(expr)}x:=expr{P(x)} While: {P ∧ B} S {P} {P} while B do S end {P ∧ (not B)} if--then--else {B ∧ P} S1 {Q}, {(not B) ∧ P} S2 {Q} {P} if B then S1 else S2{Q}