《程序的公理化证明PPT课件》由会员分享，可在线阅读，更多相关《程序的公理化证明PPT课件（15页珍藏版）》请在金锄头文库上搜索。
1、程序的公理化证明赵建华南京大学计算机系简介C.A.R. Hoare提出的公理系统断言中包含了逻辑公式和代码组合式证明先证明程序的各个部分，然后把这些证明组合起来，得到更大代码的证明。本证明系统基于某个一阶推理系统.断言的形式Hoare三元式P S QS ：代码P(pre-condition，前置条件)Q (post-condition，后置条件)P和Q是一阶逻辑公式三元式指出了一个部分正确性如果S从一个满足P的状态开始执行，且S 能够正常执行完毕，那么最后的状态满足Q。程序的抽象语法基本语句赋值语句：v:=eskip语句复合语句顺序：S;S选择：if p then S else S fi循环：
2、while p do S公理：赋值语句Qe/v v:=e Q如果语句v:=e执行之前的状态满足 Qe/v，那么v:=e执行之后的状态满足Q。Qe/v表示将公式Q中的v替换成为e后得到的公式。例如：x+1=10x:=x+1x=10公理：skip语句skip语句不改变状态。P skip Ppre,post规则在证明了一个断言之后，我们可以弱化其后置条件，或者强化其前置条件。P=P，P S QP S QP S Q，Q = QP S Q顺序组合规则在证明一个顺序组合语句的时候，我们可以先分别证明两个子语句的性质，然后将其合并得到整个组合语句的性质。P S1 Q， QS2RP S1;S2 Rif-the
3、n-else规则Pp S1 Q ，Pp S2 Q P if p then S1 else S2 Qif语句的语义是：如果p成立，则执行S1，否则执行S2。前提条件表明如果开始状态满足Pp那么执行了S1 之后满足Q。如果开始状态满足Pp，那么执行S之后仍然满足Q。如果开始状态满足P，那么它要么满足Pp，要么满足Pp。从if语句的含义我们可以知道结论成立。while规则(部分正确性)Pp S PPwhile p do S PP被称为while语句的不变式。在while语句的执行过程中，这个性质总是成立。而while语句会执行到p不成立为止。因此，当while语句退出循环时，状态必然满足Pp。这个性
4、质不保证whilewhile语句会退出循环while规则(完全正确性)如果能够找到一个函数ff的取值和变量取值有关，且Pp f0且对任意的常数f0，f=f0 S ff0,那么循环必然终止for(int i = 0; ix2 doy1:=y1+1;y2:=y2-x2end要证明如下结论：当x1=0, x2=0成立时，最终得到的y1是x1/x2的整数商部分，y2是x1/x2的余数部分即：Precondition: x1=0 x2=0Postcondition：x1=y1*x2+y2 y2=0 y2=0 x20y1=0;x1=0 x20 y1=0y2=x1;x1=y1*x2+y2 y2=0while y2=x2 dox1=y1*x2+y2 y2=x2y1:=y1+1;x1=y1*x2+y2-x2 y2=x2 y2:=y2-x2x1=y1*x2+y2 y2=0 endx1=y1*x2+y2 y2=0 y2x2 练习考虑辗转相除法求解GCD的算法的正确性证明考虑图论中最短路径的Floyd算法的正确性。Hoare Logic不能处理指针/数组反例1：true mm2 := 3 mm2 = 3当原来m2=2时，赋值之后，m2等于3，mm2的值是原来的m3，不一定等于3！反例2：*p = *q *p:=*p+1 *p = *q+1当p和q指向同一个位置时，结果应该是*p=*q仍然成立。
