Hoare逻辑 ·部分正确性的证明规则 赋值公理 {Q[Elx]x={2) 赋值公理的实例 -{2=2}x=2{x=2} -{2==4}X=2{x=4} -{2=y}x=2{x=y} -{2>0}x=2{x>0》 -{x+1+5=y}x=x+1{x+5==y} {x+1>0人y>0}X=x+1{x>0Λy>0Hoare逻辑 • 部分正确性的证明规则 – 赋值公理 赋值公理的实例 – { 2 == 2 } x = 2 { x == 2 } – { 2 == 4 } x = 2 { x == 4 } – { 2 == y } x = 2 { x == y } – { 2 > 0 } x = 2 { x > 0 } – { x + 1 + 5 == y } x = x + 1 { x + 5 ==y } – { x + 1 > 0  y > 0 } x = x + 1 { x > 0  y > 0 } { Q[E/x] } x = E { Q }