Hoare逻辑 ·部分正确性的证明规则 -推论规则 ARP→P{P}C{2} AR2→2 {P}C{2} ARP'→P表示P→P在谓词逻辑的自然演绎演 算中可以证明Hoare逻辑 • 部分正确性的证明规则 – 推论规则 AR P P 表示P P在谓词逻辑的自然演绎演 算中可以证明 AR P P { P } C { Q } AR Q  Q { P } C { Q }