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 ! }