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