《程序的公理化证明》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:=eskip语句复合语句顺序：S;S选择：ifpthenSelseSfi循环：w

2、hilepdoS公理：赋值语句{Q[e/v]}v:=e{Q}如果语句v:=e执行之前的状态满足Q[e/v]，那么v:=e执行之后的状态满足Q。Q[e/v]表示将公式Q中的v替换成为e后得到的公式。例如：{x+1==10}x:=x+1{x==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}，{Q}S2{R}{P}S1;S2{R}if-then-else规则{P∧p}S1{Q}，{P∧┒p}S2{Q}{P}ifpthenS1elseS2{Q}if语句的语义是：如果p成立，则执行S1，否则执行S2。前提条件表明如果开始状态满足P∧p那么执行了S1之后满足Q。如果开始状态满足P∧┒p，那么执行S之后仍然满足Q。如果开始状态满足P，那么它要么满足P∧p，要么满足P∧┒p。从if语句的含义我们可以知道结论成立。while规则(部分正确性){P∧p}S{P}{P}whilepdoS{φ∧┒P}P被称为while语句的不变式。在while语句的执行过程中，

4、这个性质总是成立。而while语句会执行到p不成立为止。因此，当while语句退出循环时，状态必然满足P∧┒p。这个性质不保证while语句会退出循环while规则(完全正确性)如果能够找到一个函数ff的取值和变量取值有关，且P∧pf>0且对任意的常数f0，{f=f0}S{fx2doy1:=y1+1;y2:=y2-x2end要证明如下结论：当x1>=0,x2>=0成立时，最终得到的y1是x1/x2的整数商部分，y2是x1/x2的余数部分即：Pr

5、econdition:x1>=0∧x2>=0Postcondition：x1=y1*x2+y2∧y2>=0∧y2=0∧x2>0}y1=0;{x1>=0∧x2>0∧y1=0}y2=x1;{x1=y1*x2+y2∧y2>=0}whiley2>=x2do{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∧y2

6、算法的正确性。HoareLogic不能处理指针/数组反例1：{true}m[m[2]]:=3{m[m[2]]==3}当原来m[2]=2时，赋值之后，m[2]等于3，m[m[2]]的值是原来的m[3]，不一定等于3！反例2：{*p==*q}*p:=*p+1{*p==*q+1}当p和q指向同一个位置时，结果应该是*p==*q仍然成立。