Hoare逻辑 ●例1Succ ●例2Fac1 {} {x>=0} a=x+1; y=1; if(a-1=0){ Z=0; y=1; while (Z!=x){ else Z=Z+1; y=a; y=y*Z巧 {y=x+1} {y=x!
Hoare逻辑 • 例1 Succ • 例2 Fac1 { } { x >= 0 } a = x + 1; y = 1; if (a -1 == 0 ) { z = 0; y = 1; while ( z != x ) { } else { z = z + 1; y = a; y = y z; } } { y == x + 1 } { y == x ! }
Hoare逻辑 ●例2Fac1 ●例3Fac2 {x>=0} x是辅助的逻辑变量 y=1; {x>=0入x=X0} z=0; y=1; while (Z!=x){ while (x!=0){ z=Z+1; y=y*x; y=y*Z到 x=x-1; {y=x!} {y==xo!}
Hoare逻辑 • 例2 Fac1 • 例3 Fac2 { x >= 0 } x0是辅助的逻辑变量 y = 1; { x >= 0 x == x0 } z = 0; y = 1; while ( z != x ) { while ( x != 0 ) { z = z + 1; y = y x; y = y z; x = x − 1; } } { y == x ! } { y == x0 ! }
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>0
Hoare逻辑 • 部分正确性的证明规则 – 赋值公理 赋值公理的实例 – { 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 }
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}{∧-By
Hoare逻辑 • 部分正确性的证明规则 – 赋值公理 – 复合规则 – 条件规则 – 循环规则 { 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}
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 }