版权说明:本文档由用户提供并上传,收益归属内容提供方,若内容存在侵权,请进行举报或认领
文档简介
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 选择:if p t
2、hen 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 Ppre,post规则 在证明了一个断言之后,我们可以弱化其后置条件,或者强化其前置条件。P=P,P S QP S QP S Q,Q = QP S Q顺序组合规则 在证明一个顺序组合语句的时候,我们可以先分别证明两个子语句的性质,然后将其合并得到整个组合语句的性质。P
3、S1 Q, QS2RP S1;S2 Rif-then-else规则Pp S1 Q ,Pp S2 Q P if p then S1 else S2 Q if语句的语义是:如果p成立,则执行S1,否则执行S2。 前提条件表明 如果开始状态满足Pp那么执行了S1 之后满足Q。 如果开始状态满足P p,那么执行S之后仍然满足Q。 如果开始状态满足P,那么它要么满足Pp,要么满足P p。从if语句的含义我们可以知道结论成立。while规则(部分正确性)Pp S PPwhile p do S P P被称为while语句的不变式。 在while语句的执行过程中,这个性质总是成立。 而while语句会执行到p
4、不成立为止。 因此,当while语句退出循环时,状态必然满足Pp。 这个性质不保证whilewhile语句会退出循环while规则(完全正确性) 如果能够找到一个函数f f的取值和变量取值有关,且 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
温馨提示
- 1. 本站所有资源如无特殊说明,都需要本地电脑安装OFFICE2007和PDF阅读器。图纸软件为CAD,CAXA,PROE,UG,SolidWorks等.压缩文件请下载最新的WinRAR软件解压。
- 2. 本站的文档不包含任何第三方提供的附件图纸等,如果需要附件,请联系上传者。文件的所有权益归上传用户所有。
- 3. 本站RAR压缩包中若带图纸,网页内容里面会有图纸预览,若没有图纸预览就没有图纸。
- 4. 未经权益所有人同意不得将文件中的内容挪作商业或盈利用途。
- 5. 人人文库网仅提供信息存储空间,仅对用户上传内容的表现方式做保护处理,对用户上传分享的文档内容本身不做任何修改或编辑,并不能对任何下载内容负责。
- 6. 下载文件中如有侵权或不适当内容,请与我们联系,我们立即纠正。
- 7. 本站不保证下载资源的准确性、安全性和完整性, 同时也不承担用户因使用这些下载资源对自己和他人造成任何形式的伤害或损失。
最新文档
- 2024年青海2024年客运从业资格证模拟考试题答案
- 2024年陕西客运驾驶员考试虚拟场景考试题及答案
- 2024年阿拉善盟道路旅客运输驾驶员继续教育试题
- 2024年呼和浩特客运资格证仿真考试题
- 海水淡化行业市场发展趋势及投资咨询报告
- 基因治疗行业消费者群体特征分析
- 新材料科技行业竞争格局与投资战略研究咨询报告
- 区块链跨境支付行业研究报告
- 区块链与人工智能融合行业发展前景及投资风险预测分析报告
- 江西省赣州市会昌县2023-2024学年二年级上学期期末考试数学试题
- 妇产科孕期保健PDCA循环案例
- 电子信息产业发展现状、趋势及重点
- 设备验收合格标准
- 纪委监督工作培训课件
- 四年级奥数特色讲义
- 湘教版二年级上册科学教案全册
- 春节的传统习俗变迁
- 《医院部门设置》课件
- 分布式储能系统应用
- 人教鄂教五年级科学上册全册课件
- 炊事基础理论知识
评论
0/150
提交评论