对程序进行推理的逻辑计算机科学导论第二讲.ppt

《对程序进行推理的逻辑计算机科学导论第二讲.ppt》由会员分享，可在线阅读，更多相关《对程序进行推理的逻辑计算机科学导论第二讲.ppt（45页珍藏版）》请在三一办公上搜索。

1、对程序进行推理的逻辑计算机科学导论第二讲,计算机科学技术学院陈意云0551-63607043,课 程 内 容,课程内容围绕学科理论体系中的模型理论,程序理论和计算理论1.模型理论关心的问题 给定模型M，哪些问题可以由模型M解决；如何比较模型的表达能力2.程序理论关心的问题给定模型M，如何用模型M解决问题包括程序设计范型、程序设计语言、程序设计、形式语义、类型论、程序验证、程序分析等3.计算理论关心的问题给定模型M和一类问题,解决该类问题需多少资源,讲 座 提 纲,基本知识程序验证、程序逻辑、命题逻辑、谓词逻辑Hoare逻辑Hoare三元式、赋值公理、结构化语句的推理规则、推论规则生成验证条件的

2、演算最弱前条件演算、生成验证条件的演算程序验证实例演示二分查找等程序,基 本 知 识,程序测试与程序验证测试能发现程序有错；一般而言，测试不能保证程序无错程序验证：用数学的方法来证明程序的性质，提高软件可信程度演绎验证：指用逻辑推理的方法来证明程序具备所期望的性质 演绎验证可以保证程序无错程序逻辑：对程序进行推理的逻辑,基 本 知 识,命题逻辑合式公式（well-formed formula）的归纳定义:=p|()|()|()|()(1)p代表原子命题，例如 x 3,a5=10.5 原子命题具体形式与讨论的问题领域有关(2)代表一般命题，“:=”右部用“|”分隔的各部分代表命题的构成形式，如

3、0=x x 100(3),和代表合取、析取、非和蕴含运算，在确定了它们的运算优先关系后，很多情况下括号可以省略，如p(q1 q2)可简化为p q1 q2备注：采用而不是，用于描述函数类型,基 本 知 识,命题逻辑推理规则例：有关合取“”运算的推理规则(i)(e1)(e2)“i”表示合取引入规则（i:introduction）“e”表示合取消去规则（e:elimination）对和等都有各自的推理规则,谓词逻辑合式公式(1)谓词集合、函数集合（包括常量）(2)基于来定义项集 t:=x|c|f(t,t)(f)(3)归纳地定义基于（,）的合式公式:=P(t1,t2,tn)|()|()|()|()|(

4、x)|(x)(P)增加的规则全称量词和存在量词的证明规则等,基 本 知 识,Hoare 逻 辑,程序逻辑对程序进行推理的逻辑Hoare逻辑是一种程序逻辑介绍面向非常简单的编程语言（只有赋值语句、顺序语句、条件语句和循环语句）的Hoare逻辑推理规则,Hoare 逻 辑,合式公式语法形式：P S Q，称为Hoare三元式(1)S是代码段，遵循相应编程语言的语法(2)P和Q是关于程序状态（变量到值的映射）的断言，分别称为S的前断言和后断言，断言是谓词逻辑的合式公式(3)例：x=1 y 1 y 0 y 5也成立,Hoare 逻 辑,赋值公理形式：QE/x x=E Q QE/x表示Q中出现的变量x用表

5、达式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不成立,Hoare 逻 辑,结构化语句的推理规则顺序语句条件语句（也可用其它形式表示）插曲：推论规则,Hoare 逻 辑,例（用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)的所得、(

6、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,由条件语句的规则,Hoare 逻 辑,结构化语句的推理规则（续）循环语句例：用自然数加法来完成自然数相乘x=0;y=0;while(y n)/循环不变式：(x=my)(y n)x=x+m;y=y+1;/x=m n,I 被称为 循环不变式,I E 语句S和后断言I的最弱前条件：(x=my y n y n)(x+m=m(y+1)y+1 n),Hoare 逻 辑,小结用Hoare

7、逻辑，可以对简单程序进行手工证明手工体现在两方面(1)手工用推理规则进行演算或推理(2)手工进行定理证明（前例遇到蕴含式的证明）第一次讲座对自动定理证明已略有介绍如何走向自动验证（以函数的正确性验证为例）(1)函数的前条件和后条件必须由验证者给出(2)把推理规则改造成能自动演算的演算规则(3)借助自动定理证明器,生成验证条件的演算,最弱前条件（Weakest Precondition）演算WPWP:程序集 断言集 断言集 WP(S,Q)：计算P S Q的最弱前条件PHoare逻辑的赋值公理是最弱前条件演算的一条规则(1)赋值公理：QE/x x=E Q(2)赋值语句的WP演算规则：WP(x=E,

8、Q)=QE/x,生成验证条件的演算,最弱前条件演算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)称为验证条件,生成验证条件的演算,最弱前条件演算WPWP(x=E,Q)=QE/xQE/x x=E QWP(S1;S2,Q)=WP(S1,WP(S2,Q)WP(if E then S1 else S2,Q)=(WP(S1,Q)E)(WP

9、(S2,Q)E),生成验证条件的演算,最弱前条件演算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()=WP0()WP1()WP2(),WP演算在循环语句这里遇到了困难,生成验证条件的演算,最弱前条件演算WP一些其他规则(1)WP(S,false)=false(2)WP(S,Q1 Q2)=WP(S,Q1)WP(S,Q2)(3)WP(S,Q1 Q2)=WP(S,Q1)WP(S,Q2)(4)(5)WP

10、(S,true)=保证S终止的最弱前条件.下面考虑解决由循环语句引出的问题,生成验证条件的演算,生成验证条件的演算VC(verification condition)把WP演算放宽为VC演算,即并非强求最弱前条件(1)要求验证者提供循环不变式(2)VC(S,Q)强于WP(S,Q)(3)VC(S,Q)仍弱于P，即P VC(S,Q)WP(S,Q),生成验证条件的演算,生成验证条件的演算VC(verification condition)除了循环语句外，VC演算与WP的一致循环语句的VC演算如下，其中I是循环不变式VC(while E do S,Q)=I x1xn(I E VC(S,I)(I E Q

11、)其中x1,xn是在S中被修改的所有变量实际做法(1)黄色部分和绿色部分 分别作为循环出口和入口的验证条件(2)I作为继续逆向VC演算的后断言,程 序 验 证 实 例,void mult(int m,int n)x=0;y=0;while(y n)do x=x+m;y=y+1;,例子：用加运算来实现乘运算的函数,程 序 验 证 实 例,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/后条件,由程序员提供,由程序员提供,程 序 验 证 实 例,n 0void mult(int m,int n)x=0;y=0;

12、while(y n)do(x=my)(y n)/循环不变式x=x+m;y=y+1;x=m n,也由程序员提供,程 序 验 证 实 例,n 0void mult(int m,int n)x=0;y=0;while(y n)do(x=my)(y n)/循环不变式x=x+m;y=y+1;x=m n,函数前后条件、循环不变式都称为断言它们看上去像编程语言的布尔表达式,程 序 验 证 实 例,n 0void mult(int m,int n)x=0;y=0;while(y n)do(x=my)(y n)x=x+m;y=y+1;(x=my)(y n)(y n)/循环结束程序点的断言 x=m n,程 序 验

13、 证 实 例,n 0void mult(int m,int n)x=0;y=0;while(y n)do(x=my)(y n)x=x+m;y=y+1;(x=my)(y n)(y n)(x=mn)x=m n,第1个验证条件,程 序 验 证 实 例,n 0void mult(int m,int n)x=0;y=0;while(y n)do(x=my)(y n)x=x+m;(x=m(y+1)(y+1)n)y=y+1;(x=my)(y n)(x=my)(y n)(y n)(x=mn)x=m n,通过最弱前条件演算得到,程 序 验 证 实 例,n 0void mult(int m,int n)x=0;y

14、=0;while(y n)do(x=my)(y n)(x+m=m(y+1)(y+1)n)x=x+m;(x=m(y+1)(y+1)n)y=y+1;(x=my)(y n)(x=my)(y n)(y n)(x=mn)x=m n,程 序 验 证 实 例,n 0void mult(int m,int n)x=0;y=0;(x=my)(y n)(y n)(x+m=m(y+1)(y+1)n)while(y n)do(x=my)(y n)(x+m=m(y+1)(y+1)n)x=x+m;(x=m(y+1)(y+1)n)y=y+1;(x=my)(y n)(x=my)(y n)(y n)(x=mn)x=m n,第2

15、个验证条件,程 序 验 证 实 例,n 0void mult(int m,int n)x=0;(x=m0)(0 n)y=0;(x=my)(y n)(y n)(x+m=m(y+1)(y+1)n)while(y n)do(x=my)(y n)(x+m=m(y+1)(y+1)n)x=x+m;(x=m(y+1)(y+1)n)y=y+1;(x=my)(y n)(x=my)(y n)(y n)(x=mn)x=m n,程 序 验 证 实 例,n 0void mult(int m,int n)(0=m0)(0 n)x=0;(x=m0)(0 n)y=0;(x=my)(y n)(y n)(x+m=m(y+1)(y

16、+1)n)while(y n)do(x=my)(y n)(x+m=m(y+1)(y+1)n)x=x+m;(x=m(y+1)(y+1)n)y=y+1;(x=my)(y n)(x=my)(y n)(y n)(x=mn)x=m n,程 序 验 证 实 例,n 0void mult(int m,int n)(n 0)(0=m0)(0 n)(0=m0)(0 n)x=0;(x=m0)(0 n)y=0;(x=my)(y n)(y n)(x+m=m(y+1)(y+1)n)while(y n)do(x=my)(y n)(x+m=m(y+1)(y+1)n)x=x+m;(x=m(y+1)(y+1)n)y=y+1;(

17、x=my)(y n)(x=my)(y n)(y n)(x=mn)x=m n,第3个验证条件,程 序 验 证 实 例,n 0void mult(int m,int n)(n 0)(0=m0)(0 n)x=0;y=0;(x=my)(y n)(y n)(x+m=m(y+1)(y+1)n)while(y n)do(x=my)(y n)x=x+m;y=y+1;(x=my)(y n)(y n)(x=mn)x=m n,由自动定理证明器完成验证条件的证明,程 序 验 证 实 例,程序：二分查找val=38,i=0,j=14,k=7i=0;j=14;while(i=ak)i=k+1;if(i 1 j)找到 el

18、se 没有找到,程 序 验 证 实 例,程序：二分查找val=38,i=0,j=6,k=3i=0;j=14;while(i=ak)i=k+1;if(i 1 j)找到 else 没有找到,程 序 验 证 实 例,程序：二分查找val=38,i=4,j=6,k=5i=0;j=14;while(i=ak)i=k+1;if(i 1 j)找到 else 没有找到,程 序 验 证 实 例,程序：二分查找val=38,i=6,j=6,k=6i=0;j=14;while(i=ak)i=k+1;if(i 1 j)找到 else 没有找到,程 序 验 证 实 例,程序：二分查找val=38,i=6,j=5,k=6

19、i=0;j=14;while(i=ak)i=k+1;if(i 1 j)找到 else 没有找到,程 序 验 证 实 例,程序：二分查找val=37,i=4,j=6,k=5（若val改成37）i=0;j=14;while(i=ak)i=k+1;if(i 1 j)找到 else 没有找到,程 序 验 证 实 例,程序：二分查找val=37,i=6,j=4,k=5（若val改成37）i=0;j=14;while(i=ak)i=k+1;if(i 1 j)找到 else 没有找到,程 序 验 证 实 例,程序：二分查找的主要程序段和断言int i,j,k,val,am;/此前有#define m=15m

20、 0 i=0 j=m1 n:0.m2.an an ji=2 k=i1 val=ak)/循环不变式 k=i+(j i)/2;/包括黄色部分 if(val=ak)i=k+1;n:0.m2.an an+1(ij=2 k=i1 val=ak ij=1 n:0.m1.val!=an),程 序 验 证 实 例,原型系统验证实例一维数组快速排序程序、冒泡排序、二分查找、二叉堆等易变数据结构下面这些数据类型的插入函数和删除函数等1、单链表、循环单链表2、双向变量、循环双向链表3、二叉排序树、平衡树(AVL tree)、AA 树、树堆(treap)、伸展树(splay tree)原型系统网址,小 结,本讲座小结

21、介绍怎样从Hoare逻辑得到一种对应的演算，最终得到自动证明程序是否具备所期望性质的一种方法程序验证的应用情况例举空客公司在A400M军用航空器以及A380和A350商用航空器的开发上，已经用形式证明取代了部分安全攸关嵌入式软件的测试达索航空公司在健壮性的形式验证方面，有约15%的断言是用演绎验证方式证明的相关课程：程序设计语言基础、程序设计语言理论,小 结,研究方向提高断言语言的表达能力提高自动定理证明器的证明能力工具实验室：ESC/Java、Spec#、Ynot和Why3等工业界开始应用的有Caveat、Frama-C和SPARK参考文献何伟等译，面向计算机科学的数理逻辑，2007.Yannick Moy,etc.Testing or Formal Verification:DO-178C Alternatives and Industrial Experience.IEEE Software,30(3):50-57,2013.,