《对程序进行推理的逻辑计算机科学导论第二讲ppt课件.ppt》由会员分享，可在线阅读，更多相关《对程序进行推理的逻辑计算机科学导论第二讲ppt课件.ppt（57页珍藏版）》请在taowenge.com淘文阁网|工程机械CAD图纸|机械工程制图|CAD装配图下载|SolidWorks_CaTia_CAD_UG_PROE_设计图分享下载上搜索。
1、对程序进行推理的逻辑计算机科学导论第二讲ppt课件 Still waters run deep.流静水深流静水深,人静心深人静心深 Where there is life,there is hope。有生命必有希望。有生命必有希望课课 程程 内内 容容课程内容课程内容围绕学科理论体系中的模型理论围绕学科理论体系中的模型理论,程序理论和计算理论程序理论和计算理论1.模型理论关心的问题模型理论关心的问题 给定模型给定模型M，哪些问题可以由模型，哪些问题可以由模型M解决；如何解决；如何比较模型的表达能力比较模型的表达能力2.程序理论关心的问题程序理论关心的问题给定模型给定模型M，如何用模型，如何用模
2、型M解决问题解决问题包括程序设计范型、包括程序设计范型、程序设计语言程序设计语言、程序设计、程序设计、形式语义、类型论、形式语义、类型论、程序验证程序验证、程序分析程序分析等等3.计算理论关心的问题计算理论关心的问题给定模型给定模型M和一类问题和一类问题,解决该类问题需多少资源解决该类问题需多少资源2 本次讲座讨论怎样用数本次讲座讨论怎样用数学方法证明程序是正确的学方法证明程序是正确的讲讲 座座 提提 纲纲基本知识基本知识程序验证、程序逻辑、命题逻辑、谓词逻辑程序验证、程序逻辑、命题逻辑、谓词逻辑Hoare逻辑逻辑Hoare三元式、赋值公理、结构化语句的推理规则、三元式、赋值公理、结构化语句的
3、推理规则、推论规则推论规则生成验证条件的演算生成验证条件的演算最弱前条件演算、生成验证条件的演算最弱前条件演算、生成验证条件的演算程序验证实例演示程序验证实例演示二分查找程序二分查找程序3序序 曲曲近几年近几年软软件件错误带错误带来危害的事例来危害的事例2012年，美国年，美国KCP金融公司由于电子交易系统出金融公司由于电子交易系统出现故障，交易算法出错，导致该公司对现故障，交易算法出错，导致该公司对150支不同支不同的股票高价购进、低价抛出，直接给公司带来了的股票高价购进、低价抛出，直接给公司带来了4.4亿美元的损失，当天股票下跌亿美元的损失，当天股票下跌62%2013年年9月月12日，美联
4、航售票网站一度出现问题，日，美联航售票网站一度出现问题，售出票面价格为售出票面价格为0-10美元的超低价机票，引发抢美元的超低价机票，引发抢购。大约购。大约15分钟后，美联航发现错误，关闭售票分钟后，美联航发现错误，关闭售票网站并声称正在进行维护。大约两个多小时后，网站并声称正在进行维护。大约两个多小时后，该公司售票网站恢复正常，并且承认已卖出的票该公司售票网站恢复正常，并且承认已卖出的票有效有效4序序 曲曲软软件件错误带错误带来危害的事例来危害的事例据据自然自然杂志网站报道，广受世界天文学界期杂志网站报道，广受世界天文学界期待的日本旗舰级天文卫星待的日本旗舰级天文卫星“瞳瞳”（Hitomi）
5、于）于2016年年2月月17日发射升空，但在大约日发射升空，但在大约5周之后便出周之后便出现翻滚失控迹象。经调查后日本方面宣布，事故现翻滚失控迹象。经调查后日本方面宣布，事故原因源自底层软件错误。卫星的控制系统在发现原因源自底层软件错误。卫星的控制系统在发现飞行姿态失控时，采取了错误的调整，推进器点飞行姿态失控时，采取了错误的调整，推进器点火时朝向了错误的反方向，导致自身旋转更加严火时朝向了错误的反方向，导致自身旋转更加严重，最终彻底失控重，最终彻底失控5序序 曲曲软软件无件无处处不在不在全世界有超过全世界有超过10亿辆汽车在行驶，每辆新汽车上亿辆汽车在行驶，每辆新汽车上都有都有2080个微处
6、理器，有多达个微处理器，有多达3000万行的代码万行的代码在运行在运行全世界每年有多达全世界每年有多达23亿次手术，在每个现代亿次手术，在每个现代医医疗疗设备上往往会有超过设备上往往会有超过30万行的代码在运行万行的代码在运行全世界有超过全世界有超过3000辆高速列车在行驶辆高速列车在行驶，每辆列车每辆列车上会有多达上会有多达6000万行的代码在运行万行的代码在运行全世界有超过全世界有超过300万架飞机，新型飞机上会有多达万架飞机，新型飞机上会有多达2000万行代码在运行万行代码在运行如何保证这些代码没有如何保证这些代码没有错误？错误？6基基 本本 知知 识识程序：在数组程序：在数组a中快速查
7、找某个值中快速查找某个值int am n:0.m 2.an 0)的各种情况都要测试吗？的各种情况都要测试吗？对对a中出现的各个元素都需要测试吗？中出现的各个元素都需要测试吗？对对a中不出现的元素要测多少种情况？中不出现的元素要测多少种情况？10 15 21 28 32 37 44 49 53 57 62 67 71 77 837基基 本本 知知 识识程序程序测试测试与程序与程序验证验证测试测试能能发现发现程序有程序有错错；一般而言，；一般而言，测试测试不能保不能保证证程序无程序无错错程序验证：用数学的方法来证明程序的性质，提程序验证：用数学的方法来证明程序的性质，提高软件可信程度高软件可信程度
8、演绎验证演绎验证：指用逻辑推理的方法指用逻辑推理的方法来来证明程序证明程序具备具备所期望所期望的性质的性质就所期望的性质而言，就所期望的性质而言，演绎验证演绎验证可保证程序无错可保证程序无错程序程序逻辑逻辑：对对程序程序进进行推理的行推理的逻辑逻辑 8基基 本本 知知 识识命题逻辑命题逻辑程序设计中用到命题逻辑的知识程序设计中用到命题逻辑的知识if(0=m&m 100)0=m和和m 100都是命题逻辑的都是命题逻辑的原子命题原子命题&是命题逻辑的二元是命题逻辑的二元运算符运算符(下面用下面用 而非而非&)if(0 m|0=100);n=n+1;!是命题逻辑的一元是命题逻辑的一元运算符运算符（下
9、面用（下面用 而不是而不是!）9基基 本本 知知 识识命题逻辑命题逻辑合式公式（合式公式（well-formed formula）的归纳定义）的归纳定义 :=p|()(1)p代表原子命代表原子命题题，例如，例如 x 3,a5=10.5 原子命原子命题题具体形式与具体形式与讨论讨论的的问题领问题领域有关域有关(2)代表一般命代表一般命题题，“:=”右部用右部用“|”分隔的各部分隔的各部分代表命分代表命题题的构成形式，如的构成形式，如 0=x x 100(3),和和代表合取、析取、非和代表合取、析取、非和蕴蕴涵运算，涵运算，在确定了它在确定了它们们的运算的运算优优先关系后，很多情况下括先关系后，很
10、多情况下括号可以省略，如号可以省略，如p (q1 q2)可可简简化化为为p q1 q2备备注：注：蕴蕴涵采用涵采用而不是而不是，用于描述函数用于描述函数类类型型 10基基 本本 知知 识识命题逻辑命题逻辑推理推理规则规则例：有关合取例：有关合取“”运算的推理运算的推理规则规则(i)(e1)(e2)“i”表示合取引入表示合取引入规则规则（i:introduction）“e”表示合取消去表示合取消去规则规则（e:elimination）对对 和和 等也都有各自的推理等也都有各自的推理规则规则 11谓词逻辑谓词逻辑程序设计中用到谓词逻辑的知识程序设计中用到谓词逻辑的知识谓词：结果类型为谓词：结果类型
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 )例如例如 a+5 b 3中的中的a+5和和b 3(3)归纳地定义基于（归纳地定义基于（,）的合式公
12、式）的合式公式 :=P(t1,t2,tn)|x|x|()(P )增加的规则增加的规则全称量全称量词词断言和存在量断言和存在量词词断言的断言的证证明明规则规则等等基基 本本 知知 识识13Hoare 逻逻 辑辑程序程序逻辑逻辑对程序进行推理的逻辑对程序进行推理的逻辑Hoare逻辑是一种程序逻辑逻辑是一种程序逻辑介绍面向非常简单的编程语言（只有赋值语句、介绍面向非常简单的编程语言（只有赋值语句、顺序语句、条件语句和循环语句）的顺序语句、条件语句和循环语句）的Hoare逻辑推逻辑推理规则理规则14Hoare 逻逻 辑辑合式公式（合式公式（well-formed formula）语语法形式：法形式：P
13、 S Q，称，称为为Hoare三元式三元式(1)S是代是代码码段段，遵循相，遵循相应编应编程程语语言的言的语语法法(2)P和和Q是关于程序状是关于程序状态态（变变量到量到值值的映射）的的映射）的断言断言，分，分别别称称为为S的前断言和后断言，断言是的前断言和后断言，断言是谓词谓词逻辑逻辑的合式公式的合式公式(3)例：例：x=1 y 5 x=x+1 x=2 y 5P S Q的含的含义义：在：在满满足足P的状的状态态下下执执行行S，若，若执执行行终终止，止，则终则终止状止状态满态满足足Q例：例：x=1 y 5 x=x+1 x=2 y 1 y 0 y 6 x=x+1 x 6 是赋值公理的实例是赋值公
14、理的实例特点：特点：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不成立不成立16Hoare 逻逻 辑辑结结构化构化语语句的推理句的推理规则规则顺顺序序语语句句条件条件语语句（也可用其它形式表示）句（也可用其它形式表示）插曲：推插曲：推论规则论规则P P P S Q Q Q P S Q P E S1 Q P E S2 QP
15、 if E then S1 else S2 QP S1 R R S2 QP S1;S2 Q17Hoare 逻逻 辑辑例（用例（用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=
16、yP E S1 Q P E S2 QP if E then S1 else S2 Q 由条件语句由条件语句的规则的规则18Hoare 逻逻 辑辑结结构化构化语语句的推理句的推理规则规则（续续）循循环语环语句句例：用自然数加法来完成自然数例：用自然数加法来完成自然数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 nI E S II while E do S IEI 被称为被称为 循环不变式循环不变式19/循循环环不不变变式式I：(x=m y)(y n)Ho
17、are 逻逻 辑辑结结构化构化语语句的推理句的推理规则规则（续续）循循环语环语句句例：用自然数加法来完成自然数例：用自然数加法来完成自然数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 nI E S II while E do S IEI 被称为被称为 循环不变式循环不变式20/循循环环不不变变式式I：(x=m y)(y n)分两步看，对于分两步看，对于y=y+1Hoare 逻逻 辑辑结结构化构化语语句的推理句的推理规则规则（续续）循循环语环语句句例：用
18、自然数加法来完成自然数例：用自然数加法来完成自然数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 nI E S II while E do S IEI 被称为被称为 循环不变式循环不变式21/循循环环不不变变式式I：(x=m y)(y n)分两步看，对于分两步看，对于x=x+mHoare 逻逻 辑辑结结构化构化语语句的推理句的推理规则规则（续续）循循环语环语句句例：用自然数加法来完成自然数例：用自然数加法来完成自然数m和和n相乘相乘x=0;y=0;whi
19、le(y n)x=x+m;y=y+1;/x=m n 证证明明I E 语语句句S和后断言和后断言I的最弱前条件：的最弱前条件：I E S II while E do S IEI 被称为被称为 循环不变式循环不变式22/循循环环不不变变式式I：(x=m y)(y n)(x=m y y n y n)(x+m=m(y+1)y+1 n)最后一行称为验证条件最后一行称为验证条件Hoare 逻逻 辑辑小结小结用用Hoare逻辑，可对简单程序进行逻辑，可对简单程序进行手工推理证明手工推理证明手工体现在两方面手工体现在两方面(1)手工用推理规则进行演算或推理手工用推理规则进行演算或推理(2)手工进行验证条件的证
20、明（前例遇到蕴涵式的手工进行验证条件的证明（前例遇到蕴涵式的证明，证明，第一讲对自动定理证明已略有介绍）第一讲对自动定理证明已略有介绍）虽是证明程序的一种方法，但低效、不能接受虽是证明程序的一种方法，但低效、不能接受如何走向如何走向自动验证自动验证（以函数的正确性验证为例）（以函数的正确性验证为例）(1)函数的前条件和后条件必函数的前条件和后条件必须须由由验证验证者者给给出出(2)把把Hoare逻辑规则逻辑规则改成能自改成能自动动推演的演算推演的演算规则规则(3)借助自借助自动动定理定理证证明器明器证证明明验证验证条件条件23生成验证条件的演算生成验证条件的演算最弱前条件（最弱前条件（Weak
21、est Precondition）演算）演算WP函数函数WP:程序集程序集 断言集断言集 断言集断言集 WP(S,Q)：计算：计算P S Q的最弱前条件的最弱前条件PHoare逻辑的赋值公理直接是最弱前条件演算的一逻辑的赋值公理直接是最弱前条件演算的一条规则条规则(1)赋值公理：赋值公理：QE/x x=E Q(2)赋值语句的赋值语句的WP演算规则：演算规则：WP(x=E,Q)=QE/x24生成验证条件的演算生成验证条件的演算最弱前条件演算最弱前条件演算WP若一个函数的前后条件是若一个函数的前后条件是P和和Q，函数的代码是赋，函数的代码是赋值语句序列值语句序列S1,Sn，那么，那么(1)逆向从逆
22、向从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=E QWP(S1;S2,Q)=WP(S1,WP
23、(S2,Q)WP(if E then S1 else S2,Q)=(WP(S1,Q)E)(WP(S2,Q)E)P S1 R R S2 QP S1;S2 QP E S1 Q P E S2 QP if E then S1 else S2 Q26生成验证条件的演算生成验证条件的演算最弱前条件演算最弱前条件演算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,WPi 1(while E do S,Q)WP(
24、while E do S,Q)=WP0()WP1()WP2()I E S II while E do S IE WP演算在循环语句演算在循环语句这里遇到了困难这里遇到了困难27生成验证条件的演算生成验证条件的演算最弱前条件演算最弱前条件演算WP一些其他规则一些其他规则(1)WP(S,Q1 Q2)=WP(S,Q1)WP(S,Q2)(2)WP(S,Q1 Q2)=WP(S,Q1)WP(S,Q2)(3)(4)WP(S,false)=false(4)和和(5)较难理解较难理解,不介绍不介绍(5)WP(S,true)=保证保证S终止的最弱前条件终止的最弱前条件 .下面考虑解决由循环语句引出的问题下面考虑解
25、决由循环语句引出的问题Q Q WP(S,Q)WP(S,Q)28生成验证条件的演算生成验证条件的演算生成验证条件的演算生成验证条件的演算VC(verification condition)(1)观察观察P和和WP之间的关系之间的关系(2)寻找两者之间的一种称为寻找两者之间的一种称为VC(S,Q)的演算的演算(3)即即P VC(S,Q)WP(S,Q)(4)VC演算的特点：要求验证者提供循环不变式演算的特点：要求验证者提供循环不变式falsetruestrongweak Precondition(S,Q)最弱前条件最弱前条件 WP(S,Q)验证者提供的前条件验证者提供的前条件P验证条件演算结果验证条
26、件演算结果VC(S,Q)29生成验证条件的演算生成验证条件的演算生成验证条件的演算生成验证条件的演算VC(verification condition)除了循环语句外，除了循环语句外，VC演算与演算与WP的一致的一致循环语句的循环语句的VC演算如下，其中演算如下，其中I是循环不变式是循环不变式VC(while E do S,Q)=I x1xn(I E VC(S,I)(I E Q)其中其中x1,xn是在是在S中被修改的所有变量中被修改的所有变量实际做法实际做法(1)黄色部分和绿色部分黄色部分和绿色部分 分别作为循环出口和入口的验证条件分别作为循环出口和入口的验证条件(2)I作为继续逆向作为继续逆
27、向VC演算的后断言演算的后断言I E S II while E do S IE30程程 序序 验验 证证 实实 例例void mult(int m,int n)x=0;y=0;while(y n)do x=x+m;y=y+1;例子：用加运算来例子：用加运算来实现乘运算的函数实现乘运算的函数31程程 序序 验验 证证 实实 例例n 0/前条件前条件void mult(int m,int n)x=0;y=0;while(y n)do x=x+m;y=y+1;x=m n /后条件后条件由程序员提供由程序员提供由程序员提供由程序员提供由程序员提供由程序员提供由程序员提供由程序员提供32程程 序序 验验
28、 证证 实实 例例n 0void mult(int m,int n)x=0;y=0;while(y n)do (x=m y)(y n)/循环不变式循环不变式x=x+m;y=y+1;x=m n也由程序员提供也由程序员提供33程程 序序 验验 证证 实实 例例n 0void mult(int m,int n)x=0;y=0;while(y n)do (x=m y)(y n)/循环不变式循环不变式x=x+m;y=y+1;x=m n函数前后条件、循环不变式函数前后条件、循环不变式都称为断言都称为断言它们看上去像编程语言的布它们看上去像编程语言的布尔表达式尔表达式34程程 序序 验验 证证 实实 例例n
29、 0void mult(int m,int n)x=0;y=0;while(y n)do (x=m y)(y n)x=x+m;y=y+1;(x=m y)(y n)(y n)/循环结束程序点的断循环结束程序点的断言言 x=m n I E 35程程 序序 验验 证证 实实 例例n 0void mult(int m,int n)x=0;y=0;while(y n)do (x=m y)(y n)x=x+m;y=y+1;(x=m y)(y n)(y n)(x=m n)x=m nI E Q（Q是函数后条件）是函数后条件）第第1个验证条件个验证条件36程程 序序 验验 证证 实实 例例n 0void mul
30、t(int m,int n)x=0;y=0;while(y n)do (x=m y)(y n)x=x+m;(x=m(y+1)(y+1)n)y=y+1;(x=m y)(y n)(x=m y)(y n)(y n)(x=m n)x=m n 通过最弱前通过最弱前条件演算得到条件演算得到37程程 序序 验验 证证 实实 例例n 0void mult(int m,int n)x=0;y=0;while(y n)do (x=m y)(y n)(x+m=m(y+1)(y+1)n)x=x+m;(x=m(y+1)(y+1)n)y=y+1;(x=m y)(y n)(x=m y)(y n)(y n)(x=m n)x=
31、m n38程程 序序 验验 证证 实实 例例n 0void mult(int m,int n)x=0;y=0;I E VC(S,I)（S是循环体）是循环体）(x=m y)(y n)(y n)(x+m=m(y+1)(y+1)n)while(y n)do (x=m y)(y n)(x+m=m(y+1)(y+1)n)x=x+m;(x=m(y+1)(y+1)n)y=y+1;(x=m y)(y n)(x=m y)(y n)(y n)(x=m n)x=m n第第2个验证条件个验证条件39程程 序序 验验 证证 实实 例例n 0void mult(int m,int n)x=0;(x=m 0)(0 n)y=
32、0;(x=m y)(y n)(y n)(x+m=m(y+1)(y+1)n)while(y n)do (x=m y)(y n)(x+m=m(y+1)(y+1)n)x=x+m;(x=m(y+1)(y+1)n)y=y+1;(x=m y)(y n)(x=m y)(y n)(y n)(x=m n)x=m n40程程 序序 验验 证证 实实 例例n 0void mult(int m,int n)(0=m 0)(0 n)x=0;(x=m 0)(0 n)y=0;(x=m y)(y n)(y n)(x+m=m(y+1)(y+1)n)while(y n)do (x=m y)(y n)(x+m=m(y+1)(y+1
33、)n)x=x+m;(x=m(y+1)(y+1)n)y=y+1;(x=m y)(y n)(x=m y)(y n)(y n)(x=m n)x=m n41程程 序序 验验 证证 实实 例例n 0 P VC(S,I)void mult(int m,int n)(n 0)(0=m 0)(0 n)(0=m 0)(0 n)x=0;(x=m 0)(0 n)y=0;(x=m y)(y n)(y n)(x+m=m(y+1)(y+1)n)while(y n)do (x=m y)(y n)(x+m=m(y+1)(y+1)n)x=x+m;(x=m(y+1)(y+1)n)y=y+1;(x=m y)(y n)(x=m y)
34、(y n)(y n)(x=m n)x=m n第第3个验证条件个验证条件P是函数前条件，是函数前条件，S是循环之前的语是循环之前的语句序列句序列42程程 序序 验验 证证 实实 例例n 0void mult(int m,int n)(n 0)(0=m 0)(0 n)x=0;y=0;(x=m y)(y n)(y n)(x+m=m(y+1)(y+1)n)while(y n)do (x=m y)(y n)x=x+m;y=y+1;(x=m y)(y n)(y n)(x=m n)x=m n 由自动定理证明器由自动定理证明器由自动定理证明器由自动定理证明器完成验证条件的证明完成验证条件的证明完成验证条件的证
35、明完成验证条件的证明43程程 序序 验验 证证 实实 例例程序：二分查找程序：二分查找#define m 15int am n:0.m 2.an an+1用二分法在数组用二分法在数组a15中快速查找中快速查找3810 15 21 28 32 37 44 49 53 57 62 67 71 77 8344程程 序序 验验 证证 实实 例例程序：二分查找程序：二分查找val=38,i=0,j=14,k=7i=0;j=14;while(i=j)k=i+(j i)/2;if(val=ak)i=k+1;if(i 1 j)找到找到 else 没有找到没有找到10 15 21 28 32 37 44 49
36、53 57 62 67 71 77 83ijk观察点观察点45程程 序序 验验 证证 实实 例例程序：二分查找程序：二分查找val=38,i=0,j=6,k=3i=0;j=14;while(i=j)k=i+(j i)/2;if(val=ak)i=k+1;if(i 1 j)找到找到 else 没有找到没有找到10 15 21 28 32 37 44 49 53 57 62 67 71 77 83ijk观察点观察点46程程 序序 验验 证证 实实 例例程序：二分查找程序：二分查找val=38,i=4,j=6,k=5i=0;j=14;while(i=j)k=i+(j i)/2;if(val=ak)i
37、=k+1;if(i 1 j)找到找到 else 没有找到没有找到10 15 21 28 32 37 44 49 53 57 62 67 71 77 83ijk观察点观察点循环不变性：循环不变性：a0到到ai-1都小于都小于38 aj+1到到a14都大于都大于3847程程 序序 验验 证证 实实 例例程序：二分查找程序：二分查找val=38,i=6,j=6,k=6i=0;j=14;while(i=j)k=i+(j i)/2;if(val=ak)i=k+1;if(i 1 j)找到找到 else 没有找到没有找到10 15 21 28 32 37 44 49 53 57 62 67 71 77 83
38、ijk观察点观察点循环不变性：循环不变性：a0到到ai-1都小于都小于38 aj+1到到a14都大于都大于3848程程 序序 验验 证证 实实 例例程序：二分查找程序：二分查找val=38,i=6,j=5,k=6i=0;j=14;while(i=j)k=i+(j i)/2;if(val=ak)i=k+1;if(i 1 j)找到找到 else 没有找到没有找到10 15 21 28 32 37 44 49 53 57 62 67 71 77 83ijk条件不成立条件不成立49程程 序序 验验 证证 实实 例例程序：二分查找程序：二分查找val=37,i=4,j=6,k=5（若（若val改成改成3
39、7）i=0;j=14;while(i=j)k=i+(j i)/2;if(val=ak)i=k+1;if(i 1 j)找到找到 else 没有找到没有找到10 15 21 28 32 37 44 49 53 57 62 67 71 77 83ijk观察点观察点循环不变性：循环不变性：a0到到ai-1都小于都小于38 aj+1到到a14都大于都大于3850程程 序序 验验 证证 实实 例例程序：二分查找程序：二分查找val=37,i=6,j=4,k=5（若（若val改成改成37）i=0;j=14;while(i=j)k=i+(j i)/2;if(val=ak)i=k+1;if(i 1 j)找到找到
40、 else 没有找到没有找到10 15 21 28 32 37 44 49 53 57 62 67 71 77 83jik条件不成立条件不成立51程程 序序 验验 证证 实实 例例程序：二分查找的主要程序段和断言程序：二分查找的主要程序段和断言int i,j,k,val,am;/此前有此前有#define m 15m=15 (n:0.m 2.an an+1)i=0 j=m 1while(i=j)m=15 (n:0.m 2.an an+1)0 i m 1 j m 1 (j i 1(n:j+1.m 1.val an)j i=2 k=i 1 val=ak)/循环不变式循环不变式,含黄色含黄色部分部分
41、 k=i+(j i)/2;if(val=ak)i=k+1;m=15 (n:0.m 2.an an+1)(i j=2 k=i 1 val=ak i j=1 n:0.m 1.val!=an)52程程 序序 验验 证证 实实 例例正在开发的程序验证系统的正在开发的程序验证系统的验证实例验证实例数组数组快速排序、冒泡排序、二分查找、二叉堆、矩阵快速排序、冒泡排序、二分查找、二叉堆、矩阵乘、矩阵分块乘等乘、矩阵分块乘等易变数据结构易变数据结构下面这些数据类型的插入函数和删除函数等下面这些数据类型的插入函数和删除函数等1、单链表、循环单链表、单链表、循环单链表2、双向变量、循环双向链表、双向变量、循环双向
42、链表3、二叉排序树、平衡树、二叉排序树、平衡树(AVL tree)、AA 树、树树、树堆堆(treap)、伸展树、伸展树(splay tree)演示二分查找的例子演示二分查找的例子53程程 序序 验验 证证 实实 例例正在开发的程序验证系统的正在开发的程序验证系统的验证实例验证实例验证二分查找需用到的引理验证二分查找需用到的引理lemma 1:int m.int bm.int value.int k.(int n:0.m-2.bn bk 0=k bn)lemma 2:int m.int bm.int value.int k.(int n:0.m-2.bn bn+1)value bk 0=k m
43、 (int n:k.m-1.value bn)自动定理证明器发现不了这样的归纳性质自动定理证明器发现不了这样的归纳性质5410 15 21 28 32 37 44 49 53 57 62 67 71 77 83k小小 结结本讲座小结本讲座小结介介绍绍怎怎样样从从Hoare逻逻辑辑得得到到对对应应的的演演算算，最最终终得得到到自自动证动证明程序是否具明程序是否具备备所期望性所期望性质质的一种方法的一种方法程序验证的应用情况例举程序验证的应用情况例举空客公司在空客公司在A400M军用航空器以及军用航空器以及A380和和A350商商用航空器的开发上，已经用形式证明取代了部分用航空器的开发上，已经用形
44、式证明取代了部分安全攸关嵌入式软件的测试安全攸关嵌入式软件的测试达索航空公司在健壮性的形式验证方面，有约达索航空公司在健壮性的形式验证方面，有约15%的断言是用演绎验证方式证明的的断言是用演绎验证方式证明的工具工具VeriFast完成完成4个工业应用案例个工业应用案例的的安全性验证安全性验证相关课程：相关课程：程序设计语言基础、程序设计语言理论程序设计语言基础、程序设计语言理论55小小 结结研究方向研究方向提高断言语言的表达能力提高断言语言的表达能力提高自动定理证明器的证明能力提高自动定理证明器的证明能力工具工具实验室：实验室：Dafny、Spec#、Ynot和和Why3等等工业界开始应用的有
45、工业界开始应用的有Caveat、Frama-C和和 SPARK201456小小 结结参考文献参考文献何伟等译，面向计算机科学的数理逻辑，何伟等译，面向计算机科学的数理逻辑，2007.Aaron R.Bradley and Zohar Manna.The Calculus of Computation:Decision Procedures with Applications to VerificationYannick Moy,etc.Testing or Formal Verification:DO-178C Alternatives and Industrial Experience.IEEE Software,30(3):50-57,2013.本次讲座的基础知识部分来自上面第本次讲座的基础知识部分来自上面第1篇参考文献篇参考文献57