《程序的公理化证明》PPT课件.ppt

1、程序的公理化证明,赵建华 南京大学计算机系,简介,C.A.R. Hoare提出的公理系统 断言中包含了逻辑公式和代码 组合式证明 先证明程序的各个部分，然后把这些证明组合起来，得到更大代码的证明。 本证明系统基于某个一阶推理系统.,断言的形式,Hoare三元式 P S Q S ：代码 P(pre-condition，前置条件) Q (post-condition，后置条件) P和Q是一阶逻辑公式 三元式指出了一个部分正确性 如果S从一个满足P的状态开始执行，且S 能够正常执行完毕，那么最后的状态满足Q。,程序的抽象语法,基本语句 赋值语句：v:=e skip语句 复合语句 顺序：S;S 选择：

2、if p then S else S fi 循环：while p do S,公理：赋值语句,Qe/v v:=e Q 如果语句v:=e执行之前的状态满足 Qe/v，那么v:=e执行之后的状态满足Q。 Qe/v表示将公式Q中的v替换成为e后得到的公式。 例如：x+1=10 x:=x+1x=10,公理：skip语句,skip语句不改变状态。 P skip P,pre,post规则,在证明了一个断言之后，我们可以弱化其后置条件，或者强化其前置条件。 P=P，P S Q P S Q P S Q，Q = Q P S Q,顺序组合规则,在证明一个顺序组合语句的时候，我们可以先分别证明两个子语句的性质，然后将

3、其合并得到整个组合语句的性质。 P S1 Q， QS2R P S1;S2 R,if-then-else规则,Pp S1 Q ，Pp S2 Q P if p then S1 else S2 Q if语句的语义是：如果p成立，则执行S1，否则执行S2。 前提条件表明 如果开始状态满足Pp那么执行了S1 之后满足Q。 如果开始状态满足Pp，那么执行S之后仍然满足Q。 如果开始状态满足P，那么它要么满足Pp，要么满足Pp。从if语句的含义我们可以知道结论成立。,while规则(部分正确性),Pp S P Pwhile p do S P P被称为while语句的不变式。 在while语句的执行过程中，这

4、个性质总是成立。 而while语句会执行到p不成立为止。 因此，当while语句退出循环时，状态必然满足Pp。 这个性质不保证while语句会退出循环,while规则(完全正确性),如果能够找到一个函数f f的取值和变量取值有关，且 Pp f0 且对任意的常数f0， f=f0 S ff0, 那么循环必然终止 for(int i = 0; i100; i+) ,例子（1）,整数除法的累减实现 y1=0; y2=x1; while y2x2 do y1:=y1+1; y2:=y2-x2 end 要证明如下结论： 当x1=0, x2=0成立时，最终得到的y1是x1/x2的整数商部分，y2是x1/x2

5、的余数部分即： Precondition: x1=0 x2=0 Postcondition：x1=y1*x2+y2 y2=0 y2x2,例子（2）,可以按照如下方式证明： x1=0 x20 y1=0; x1=0 x20 y1=0 y2=x1; x1=y1*x2+y2 y2=0 while y2=x2 do x1=y1*x2+y2 y2=x2 y1:=y1+1; x1=y1*x2+y2-x2 y2=x2 y2:=y2-x2 x1=y1*x2+y2 y2=0 end x1=y1*x2+y2 y2=0 y2x2,练习,考虑辗转相除法求解GCD的算法的正确性证明 考虑图论中最短路径的Floyd算法的正确性。,Hoare Logic不能处理指针/数组,反例1： true mm2 := 3 mm2 = 3 当原来m2=2时， 赋值之后，m2等于3