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

Click to edit Master title style,Click to edit Master text styles,Second level,Third level,Fourth level,Fifth level,*,中国科大,*,对程序进行推理的逻辑,计算机科学导论第二讲,计算机科学技术学院,陈意云,0551-,6,3607043,课 程 内 容,课程内容,围绕学科理论体系中的模型理论,程序理论和计算理论,1.,模型理论关心的问题,给定模型,M,，哪些问题可以由模型,M,解决；如何比较模型的表达能力,2.,程序理论关心的问题,给定模型,M,，如何用模型,M,解决问题,包括程序设计范型、,程序设计语言,、程序设计、形式语义、类型论、,程序验证,、,程序分析,等,3.,计算理论关心的问题,给定模型,M,和一类问题,解决该类问题需多少资源,讲 座 提 纲,基本知识,程序验证、程序逻辑、命题逻辑、谓词逻辑,Hoare,逻辑,Hoare,三元式、赋值公理、结构化语句的推理规则、推论规则,生成验证条件的演算,最弱前条件演算、生成验证条件的演算,程序验证实例演示,二分查找等程序,基 本 知 识,程序测试与程序验证,测试能发现程序有错；一般而言，测试不能保证程序无错,程序验证：用数学的方法来证明程序的性质，提高软件可信程度,演绎验证,：,指用逻辑推理的方法,来,证明程序,具备所期望,的性质,演绎验证,可以保证程序无错,程序逻辑：对程序进行推理的逻辑,基 本 知 识,命题逻辑,合式公式（,well-formed formula,）的归纳定义,:=,p,|(,)|(,)|(,)|(,),(1),p,代表原子命题，例如,x 3,a5=10.5,原子命题具体形式与讨论的问题领域有关,(2),代表一般命题，“,:=,”右部用“,|,”分隔的各部分代表命题的构成形式，如,0=x,x 100,(3),和代表合取、析取、非和蕴含运算，在确定了它们的运算优先关系后，很多情况下括号可以省略，如,p,(,q,1,q,2,),可简化为,p,q,1,q,2,备注：采用而不是,，,用于描述函数类型,基 本 知 识,命题逻辑,推理规则,例：有关合取“,”运算的推理规则,(i),(e,1,)(e,2,),“,i,”表示合取引入规则（,i:introduction,）,“,e,”表示合取消去规则（,e:elimination,）,对和,等都有各自的推理规则,谓词逻辑,合式公式,(1),谓词集合,、函数集合,（包括常量）,(2),基于,来定义项集,t,:=,x,|,c|f,(,t,t,),(,f,),(3),归纳地定义基于（,）的合式公式,:=,P,(,t,1,t,2,t,n,)|,(,)|(,)|(,)|,(,)|(,x,),|(,x,)(,P,),增加的规则,全称量词和存在量词的证明规则等,基 本 知 识,Hoare,逻 辑,程序逻辑,对程序进行推理的逻辑,Hoare,逻辑是一种程序逻辑,介绍面向非常简单的编程语言（只有赋值语句、顺序语句、条件语句和循环语句）的,Hoare,逻辑推理规则,Hoare,逻 辑,合式公式,语法形式：,P,S,Q,，称为,Hoare,三元式,(1)S,是代码段，遵循相应编程语言的语法,(2),P,和,Q,是关于程序状态（变量到值的映射）的断言，分别称为,S,的前断言和后断言，断言是谓词逻辑的合式公式,(3),例：,x=1,y 5,x=x+1 x=2,y 5,P,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,是赋值公理的实例,特点：,x+1 6,（即,x 5,）是语句,x=x+1,和后断言,x 6,的最弱前断言,(1),x 5.1,和,x 7,都可做前断言，因为都强于,x 5,x 5.1 x 5,并且,x 7 x 5,(2),若,x 4.9,作为前断言，则三元式不成立，因为,x 4.9 x 5,不成立,Hoare,逻 辑,结构化语句的推理规则,顺序语句,条件语句（也可用其它形式表示）,插曲：推论规则,P,P,P,S,Q,Q,Q,P,S,Q,P,E,S,1,Q,P,E,S,2,Q,P,if,E,then S,1,else S,2,Q,P,S,1,R,R,S,2,Q,P,S,1,;S,2,Q,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),的所得、,(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,P,E,S,1,Q,P,E,S,2,Q,P,if,E,then S,1,else S,2,Q,由条件语句,的规则,Hoare,逻 辑,结构化语句的推理规则（续）,循环语句,例：用自然数加法来完成自然数相乘,x=0;y=0;,while(y n)/,循环不变式：,(x=m,y)(y n),x=x+m;y=y+1;,/x=m,n,I,E,S,I,I,while,E,do S,I,E,I,被称为,循环不变式,I,E,语句,S,和后断言,I,的最弱前条件：,(x=m,y y n,y n),(x+m=m,(y+1)y+1 n),Hoare,逻 辑,小结,用,Hoare,逻辑，可以对简单程序进行手工证明,手工体现在两方面,(1),手工用推理规则进行演算或推理,(2),手工进行定理证明（前例遇到蕴含式的证明）,第一次讲座对自动定理证明已略有介绍,如何走向自动验证（以函数的正确性验证为例）,(1),函数的前条件和后条件必须由验证者给出,(2),把推理规则改造成能自动演算的演算规则,(3),借助自动定理证明器,生成验证条件的演算,最弱前条件（,Weakest Precondition,）演算,WP,WP,:,程序集 断言集 断言集,WP,(,S,Q,),：计算,P,S,Q,的最弱前条件,P,Hoare,逻辑的赋值公理是最弱前条件演算的一条规则,(1),赋值公理：,Q,E,/x x=,E,Q,(2),赋值语句的,WP,演算规则：,WP,(x=,E,Q,)=,Q,E,/x,生成验证条件的演算,最弱前条件演算,WP,若一个函数的前后条件是,P,和,Q,，函数的代码是赋值语句序列,S,1,S,n,，那么,(1),逆向从,S,n,到,S,1,连续使用赋值语句的,WP,规则，,WP,(,S,1,WP,(,S,n,Q,),它是保证执行上述代码段后得到,Q,的最弱前条件,(2),若,P,WP,(,S,1,WP,(,S,n,Q,),得证，则代码段,S,1,S,n,对前后条件,P,和,Q,正确,(3),P,WP,(,S,1,WP,(,S,n,Q,),称为验证条件,生成验证条件的演算,最弱前条件演算,WP,WP,(x=,E,Q,)=,Q,E,/x,Q,E,/x x=,E,Q,WP,(S,1,;S,2,Q,)=,WP,(S,1,WP,(S,2,Q,),WP,(if,E,then S,1,else S,2,Q,)=,(,WP,(S,1,Q,),E,),(,WP,(S,2,Q,),E,),P,S,1,R,R,S,2,Q,P,S,1,;S,2,Q,P,E,S,1,Q,P,E,S,2,Q,P,if,E,then S,1,else S,2,Q,生成验证条件的演算,最弱前条件演算,WP,对于,WP,(while,E,do S,Q,),，演算有可能不终止,假定,WP,k,为循环体,S,执行,k,次的演算,WP,0,(while,E,do S,Q,)=,E,Q,WP,i,(while,E,do S,Q,)=,E,WP,(S,WP,i,1,(while,E,do S,Q,),WP,()=,WP,0,(),WP,1,(),WP,2,(),I,E,S,I,I,while,E,do S,I,E,WP,演算在循环语句,这里遇到了困难,生成验证条件的演算,最弱前条件演算,WP,一些其他规则,(1),WP,(S,false,)=,false,(2),WP,(S,Q,1,Q,2,)=,WP,(S,Q,1,),WP,(S,Q,2,),(3),WP,(S,Q,1,Q,2,)=,WP,(S,Q,1,),WP,(S,Q,2,),(4),(5),WP,(S,true,)=,保证,S,终止的最弱前条件,.,下面考虑解决由循环语句引出的问题,Q,Q,WP,(S,Q,),WP,(S,Q,),生成验证条件的演算,生成验证条件的演算,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,),false,true,strong,weak,Precondition,(,S,Q,),最弱前条件,WP,(,S,Q,),验证者提供的前条件,P,验证条件,VC,(,S,Q,),生成验证条件的演算,生成验证条件的演算,VC,(,verification condition,),除了循环语句外，,VC,演算与,WP,的一致,循环语句的,VC,演算如下，其中,I,是循环不变式,VC,(while,E,do S,Q,)=,I,x,1,x,n,(,(,I,E,VC,(S,I,),(,I,E,Q,),),其中,x,1,x,n,是在,S,中被修改的所有变量,实际做法,(1),黄色部分和绿色部分,分别作为循环出口和入口的验证条件,(2),I,作为继续逆向,VC,演算的后断言,I,E,S,I,I,while,E,do S,I,E,程 序 验 证 实 例,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,0,void 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,也由程序员提供,程 序 验 证 实 例,n,0,void 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,函数前后条件、循环不变式,都称为断言,它们看上去像编程语言的布,尔表达式,程 序 验 证 实 例,n,0,void 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,程 序 验 证 实 例,n,0,void 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,n,第,1,个验证条件,程 序 验 证 实 例,n,0,void mult(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),