Hoare逻辑 ·结构化语句的推理规则 顺序语句 {P)S1{R} {R}S2{2 {PS1;S2{2 条件语句（也可用其它形式表示) {P∧ES{Q} {P∧-ES,{Q {P)if E then S1 else S2 {O) -插曲：推论规则 P'→P{PS{Q 2→2 PS{2' 17
Hoare 逻 辑 • 结构化语句的推理规则 – 顺序语句 – 条件语句（也可用其它形式表示） – 插曲：推论规则 P P {P} S {Q} Q Q {P} S {Q} {P E} S1 {Q} {P E} S2 {Q} {P} if E then S1 else S2 {Q} {P} S1 {R} {R} S2 {Q} {P} S1 ; S2 {Q} 17
Hoare逻辑 ·例（用Hoare?逻辑手工证明简单程序段） 证：{true}if(x>y)z=x;elsez=y;{z>=x∧z>=y (1)由赋值公理：{x>=X∧X>=y}z=x{z>=X人z>=y} (2)由(1)的所得、(true x>y)→(K>=x∧x>=y) 和推论规则，可得： {true∧x>y}Z=x{z>=X∧z>=y} (3)同理得：{true入(x>y)}z=y{z>=x∧Z>=y (4)由条件语句{PAES,{2}{P∧ES2{2} 的规则 {P}if E then S else S2 {O) 得：{true}if(K>y)z=x;else z=y{z>=x∧z>sy
Hoare 逻 辑 • 例（用Hoare逻辑手工证明简单程序段） 证: {true} if (x > y) z = x; else z = y; {z >= x z >= y} (1)由赋值公理:{x >= x x >=y}z = x{z >= x z >=y} (2) 由(1)的所得、(true x > y) (x >= x x >= y) 和推论规则，可得： {true x > y} z = x {z >= x z >= y} (3) 同理得: {true (x > y)} z = y {z >= x z >= y} (4) 得: {true} if (x > y) z = x; else z = y;{z >= x z >= y} {P E} S1 {Q} {P E} S2 {Q} {P} if E then S1 else S2 {Q} 由条件语句 的规则 18
Hoare逻辑 结构化语句的推理规则（续) -循环语句 INEY SI 被称为 {while E do S{I∧-E 循环不变式 -例：用自然数加法来完成自然数m和n相乘 x=0;y=0; while(y<n){/循环不变式I:(x=mxy)Ay≤n) x=x+m;y=y+1; }/x=m×n ·演算得到语句S和后断言I的最弱前条件： x+m==mx(y+1)∧y+1≤n 19
Hoare 逻 辑 • 结构化语句的推理规则（续） – 循环语句 – 例：用自然数加法来完成自然数m和n相乘 x = 0; y = 0; while (y < n) { x = x + m; y = y + 1; } // x == m n • 演算得到语句S和后断言I的最弱前条件： x+m == m(y+1) y+1 n {IE} S {I} {I} while E do S {IE} I 被称为 循环不变式 19 //循环不变式I：(x == my) (y n)
Hoare逻辑 结构化语句的推理规则（续) -循环语句 INEY SI 被称为 {while E do S{I∧-E 循环不变式 -例：用自然数加法来完成自然数m和n相乘 x=0;y=0; while(y<n){/循环不变式I:(=mxy)∧(y≤n) x=x+m;y=y+1; }/x=m×n 分两步看，对于y=y+1 ·演算得到语句S和后断言的最弱前条件： x+m==mx(y+1)∧y+1≤n 20
Hoare 逻 辑 • 结构化语句的推理规则（续） – 循环语句 – 例：用自然数加法来完成自然数m和n相乘 x = 0; y = 0; while (y < n) { x = x + m; y = y + 1; } // x == m n • 演算得到语句S和后断言I的最弱前条件： x+m == m(y+1) y+1 n {IE} S {I} {I} while E do S {IE} I 被称为 循环不变式 20 //循环不变式I：(x == my) (y n) 分两步看，对于y = y + 1