对程序进行推理的逻辑计算机科学导论第二讲ppt课件.ppt
《对程序进行推理的逻辑计算机科学导论第二讲ppt课件.ppt》由会员分享,可在线阅读,更多相关《对程序进行推理的逻辑计算机科学导论第二讲ppt课件.ppt(57页珍藏版)》请在三一办公上搜索。
1、对程序进行推理的逻辑计算机科学导论第二讲,计算机科学技术学院陈意云0551-63607043,http:/,课 程 内 容,课程内容围绕学科理论体系中的模型理论,程序理论和计算理论1.模型理论关心的问题 给定模型M,哪些问题可以由模型M解决;如何比较模型的表达能力2.程序理论关心的问题给定模型M,如何用模型M解决问题包括程序设计范型、程序设计语言、程序设计、形式语义、类型论、程序验证、程序分析等3.计算理论关心的问题给定模型M和一类问题,解决该类问题需多少资源,2,本次讲座讨论怎样用数学方法证明程序是正确的,讲 座 提 纲,基本知识程序验证、程序逻辑、命题逻辑、谓词逻辑Hoare逻辑Hoare
2、三元式、赋值公理、结构化语句的推理规则、推论规则生成验证条件的演算最弱前条件演算、生成验证条件的演算程序验证实例演示二分查找程序,3,序 曲,近几年软件错误带来危害的事例2012年,美国KCP金融公司由于电子交易系统出现故障,交易算法出错,导致该公司对150支不同的股票高价购进、低价抛出,直接给公司带来了4.4亿美元的损失,当天股票下跌62%2013年9月12日,美联航售票网站一度出现问题,售出票面价格为0-10美元的超低价机票,引发抢购。大约15分钟后,美联航发现错误,关闭售票网站并声称正在进行维护。大约两个多小时后,该公司售票网站恢复正常,并且承认已卖出的票有效,4,序 曲,软件错误带来危
3、害的事例据自然杂志网站报道,广受世界天文学界期待的日本旗舰级天文卫星“瞳”(Hitomi)于2016年2月17日发射升空,但在大约5周之后便出现翻滚失控迹象。经调查后日本方面宣布,事故原因源自底层软件错误。卫星的控制系统在发现飞行姿态失控时,采取了错误的调整,推进器点火时朝向了错误的反方向,导致自身旋转更加严重,最终彻底失控,5,序 曲,软件无处不在全世界有超过10亿辆汽车在行驶,每辆新汽车上都有2080个微处理器,有多达3000万行的代码在运行全世界每年有多达23亿次手术,在每个现代医疗设备上往往会有超过30万行的代码在运行全世界有超过3000辆高速列车在行驶,每辆列车上会有多达6000万行
4、的代码在运行全世界有超过300万架飞机,新型飞机上会有多达2000万行代码在运行如何保证这些代码没有错误?,6,基 本 知 识,程序:在数组a中快速查找某个值int amn:0.m2.an 0)的各种情况都要测试吗?对a中出现的各个元素都需要测试吗?对a中不出现的元素要测多少种情况?,7,基 本 知 识,程序测试与程序验证测试能发现程序有错;一般而言,测试不能保证程序无错程序验证:用数学的方法来证明程序的性质,提高软件可信程度演绎验证:指用逻辑推理的方法来证明程序具备所期望的性质就所期望的性质而言,演绎验证可保证程序无错程序逻辑:对程序进行推理的逻辑,8,基 本 知 识,命题逻辑程序设计中用到
5、命题逻辑的知识if(0=100);n=n+1;!是命题逻辑的一元运算符(下面用而不是!),9,基 本 知 识,命题逻辑合式公式(well-formed formula)的归纳定义:=p|()(1)p代表原子命题,例如 x 3,a5=10.5 原子命题具体形式与讨论的问题领域有关(2)代表一般命题,“:=”右部用“|”分隔的各部分代表命题的构成形式,如 0=x x 100(3),和代表合取、析取、非和蕴涵运算,在确定了它们的运算优先关系后,很多情况下括号可以省略,如p(q1 q2)可简化为p q1 q2备注:蕴涵采用而不是,用于描述函数类型,10,基 本 知 识,命题逻辑推理规则例:有关合取“”
6、运算的推理规则(i)(e1)(e2)“i”表示合取引入规则(i:introduction)“e”表示合取消去规则(e:elimination)对和等也都有各自的推理规则,11,谓词逻辑程序设计中用到谓词逻辑的知识谓词:结果类型为bool的函数bool even(int m)/用编程语言写的谓词,与数理 if(m/2*2=m)return true;/逻辑中的有区别 else return false;if(even(x)&even(y)、=、=、!=等关系算符都是谓词,基 本 知 识,12,谓词逻辑合式公式(1)谓词集合、函数集合(包括常量)(2)基于来定义项集 t:=x|c|f(t,t)(f
7、)例如 a+5 b 3中的a+5和b 3(3)归纳地定义基于(,)的合式公式:=P(t1,t2,tn)|x|x|()(P)增加的规则全称量词断言和存在量词断言的证明规则等,基 本 知 识,13,Hoare 逻 辑,程序逻辑对程序进行推理的逻辑Hoare逻辑是一种程序逻辑介绍面向非常简单的编程语言(只有赋值语句、顺序语句、条件语句和循环语句)的Hoare逻辑推理规则,14,Hoare 逻 辑,合式公式(well-formed formula)语法形式:P S Q,称为Hoare三元式(1)S是代码段,遵循相应编程语言的语法(2)P和Q是关于程序状态(变量到值的映射)的断言,分别称为S的前断言和后
8、断言,断言是谓词逻辑的合式公式(3)例:x=1 y 1 y 0 y 5也成立,15,Hoare 逻 辑,赋值公理形式:QE/x x=E Q QE/x表示Q中出现的变量x用表达式E代换例:x+1 6 x=x+1 x 6 是赋值公理的实例特点:x+1 6(即x 5)是语句x=x+1和后断言x 6 的最弱前断言(1)x 5.1和x 7都可作为前断言,因都强于x 5x 5.1 x 5 并且x 7 x 5(2)若x 4.9作为前断言,则三元式不成立,因为x 4.9 x 5不成立,16,Hoare 逻 辑,结构化语句的推理规则顺序语句条件语句(也可用其它形式表示)插曲:推论规则,17,Hoare 逻 辑,
9、例(用Hoare逻辑手工证明简单程序段)证:true if(x y)z=x;else z=y;z=x z=y(1)由赋值公理:x=x x=yz=xz=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,由条件语句的规则,18,Hoare 逻 辑,结构化语句的推理规则(续)循环语句例:用自然数加法来完成自然数m和n相乘x=0;y=0;while(y n)x=x+m;y=y+1;/x=m n 演
10、算得到语句S和后断言I的最弱前条件:x+m=m(y+1)y+1 n,I 被称为 循环不变式,19,/循环不变式I:(x=my)(y n),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,I 被称为 循环不变式,20,/循环不变式I:(x=my)(y n),分两步看,对于y=y+1,Hoare 逻 辑,结构化语句的推理规则(续)循环语句例:用自然数加法来完成自然数m和n相乘x=0;y=0;while(y n)x
11、=x+m;y=y+1;/x=m n 演算得到语句S和后断言I的最弱前条件:x+m=m(y+1)y+1 n,I 被称为 循环不变式,21,/循环不变式I:(x=my)(y n),分两步看,对于x=x+m,Hoare 逻 辑,结构化语句的推理规则(续)循环语句例:用自然数加法来完成自然数m和n相乘x=0;y=0;while(y n)x=x+m;y=y+1;/x=m n 证明I E 语句S和后断言I的最弱前条件:,I 被称为 循环不变式,22,/循环不变式I:(x=my)(y n),(x=my y n y n)(x+m=m(y+1)y+1 n),最后一行称为验证条件,Hoare 逻 辑,小结用Hoa
12、re逻辑,可对简单程序进行手工推理证明手工体现在两方面(1)手工用推理规则进行演算或推理(2)手工进行验证条件的证明(前例遇到蕴涵式的证明,第一讲对自动定理证明已略有介绍)虽是证明程序的一种方法,但低效、不能接受如何走向自动验证(以函数的正确性验证为例)(1)函数的前条件和后条件必须由验证者给出(2)把Hoare逻辑规则改成能自动推演的演算规则(3)借助自动定理证明器证明验证条件,23,生成验证条件的演算,最弱前条件(Weakest Precondition)演算WP函数WP:程序集 断言集 断言集 WP(S,Q):计算P S Q的最弱前条件PHoare逻辑的赋值公理直接是最弱前条件演算的一条
13、规则(1)赋值公理:QE/x x=E Q(2)赋值语句的WP演算规则:WP(x=E,Q)=QE/x,24,生成验证条件的演算,最弱前条件演算WP若一个函数的前后条件是P和Q,函数的代码是赋值语句序列S1,Sn,那么(1)逆向从Sn到S1连续使用赋值语句的WP规则,WP(S1,WP(Sn,Q)它是保证执行上述代码段后得到Q的最弱前条件(2)若P WP(S1,WP(Sn,Q)得证,则代码段S1,Sn对前后条件P和Q正确(3)P WP(S1,WP(Sn,Q)称为验证条件强调:P蕴涵最弱前条件即可,不必要求等于后者,25,生成验证条件的演算,最弱前条件演算WPWP(x=E,Q)=QE/xQE/x x=
14、E QWP(S1;S2,Q)=WP(S1,WP(S2,Q)WP(if E then S1 else S2,Q)=(WP(S1,Q)E)(WP(S2,Q)E),26,生成验证条件的演算,最弱前条件演算WP对于WP(while E do S,Q),演算有可能不终止 假定WPk为循环体S执行k次的演算 WP0(while E do S,Q)=E Q WPi(while E do S,Q)=E WP(S,WPi1(while E do S,Q)WP(while E do S,Q)=WP0()WP1()WP2(),WP演算在循环语句这里遇到了困难,27,生成验证条件的演算,最弱前条件演算WP一些其他规则
- 配套讲稿:
如PPT文件的首页显示word图标,表示该PPT已包含配套word讲稿。双击word图标可打开word文档。
- 特殊限制:
部分文档作品中含有的国旗、国徽等图片,仅作为作品整体效果示例展示,禁止商用。设计者仅对作品中独创性部分享有著作权。
- 关 键 词:
- 程序 进行 推理 逻辑 计算机科学 导论 第二 ppt 课件
![提示](https://www.31ppt.com/images/bang_tan.gif)
链接地址:https://www.31ppt.com/p-6329808.html