程序设计方法学--第三章-程序正确性证明.ppt

单击此处编辑母版标题样式,单击此处编辑母版文本样式,第二级,第三级,第四级,第五级,*,西南石油大学计算机科学学院,*,第三章,程序正确性证明,什么样的程序才是正确的？,如何来保证程序是正确的？,程序正确性概述,关于程序正确性的认识,根据问题的特性和软件所要实现的 功能，选择一些具有代表性的数据，设计测试用例。通过用例程序执行，去发现被测试程序的错误。,什么样的程序才是正确的？,“测试”或“调试”方法,采用,“,测试,”,方法可以发现程序中的错误，但却不能证明程序中没有错误！,因此，为保证程序的正确性，必须从理论上研究有关,“,程序正确性证明,”,的方法。,程序正确性证明发展历程,20,世纪,50,年代,Turing,开始研究,1967,年，,Floyd,和,Naur,提出不变式断言法,1969,年，,Hoare,提出公理化方法,1975,年，,Dijkstra,提出最弱前置谓词和程序推导方法，解决了断言构造难的问题，可从程序规约推导出正确程序，使正确性证明变得实用。,程序正确性理论是十分活跃的课题，不仅可,以证明顺序程序的正确性，而且还可以证明非确,定性程序，以及并行程序的正确性。,程序正确性理论,程序设计的一般过程,程序正确性理论,程序功能的精确描述,1,、程序规约：对程序所实现功能的精确描述，,由程序的前置断言和后置断言两部分组成。,2,、前置断言：程序执行前的输入应满足的条件，又称为输入断言。,3,、后置断言：程序执行后的输出应满足的条件，又称为输出断言。,程序设计过程：问题 程序规约 程序,程序规约的基本分类,非形式化程序规约,非形式化程序规约采用自然语言描述程序功能，简单、方便，但存在二义性，因此，不利于程序的正确性证明。,形式化程序规约,采用数学化的语言描述程序功能，描述精确，无二义性，便于程序的正确性证明。,程序规约的实例（,1/2,）,在书写程序规约时，使用,Q,表示前置断言，,R,表示后置断言，,S,表示问题求解的实现程序。在前置断言,Q,之前，还必须给出,Q,和,R,中所出现的标识符的必要说明。,例,1,：求数组,b0:n-1,中所有元素的最大值。,in n:integer;in b0:n-1:array of integer;out y:integer,Q:n 1,S,R:,y,MAX,（,i:0 i,n;bi),例,2,：求两个非负整数的最大公约数。,in a,b:integer;out y:integer,Q:a 0 b 0,S,R:,y,MAX,（,i:1 i min(a,b),(a mod i,0)(b mod i,0);i),程序规约的实例（,2/2,）,程序正确性定义（,1/3,）,衡量一个程序的正确性，主要看程序是否实现了问题所要求的功能。若程序实现了问题所要求的功能，则称它为正确的，否则是不正确的。,程序设计过程：问题 程序规约 程序,对程序的正确性理解，可以分为两个层次：,从广义来说，一个程序的正确性取决于该程序满足问题实际需求的程度。,从狭义而言，如果一个程序满足了它的程序规约就是正确的。,程序规约,QSR,是一个逻辑表达式，其取值为真或假，其中取值为真的含义是指：给定一段程序,S,，,若程序开始执行之前,Q,为真，,S,的执行将终止，且终止时,R,为真，则称为“程序,S,，,关于前置断言,Q,和后置断言,R,是完全正确的”。,程序正确性定义（,2/3,）,部分正确,：若对于每个使得,Q(i),为真,，,并且程序,S,计算终止的输入信息,i,，,R(i,S(i),都为真，则称程序,S,关于,Q,和,R,是部分正确的。,程序终止,：若对于每个使得,Q(i),为真的输入,i,，,程序,S,的计算都终止，则称程序,S,关于,Q,是终止的。,完全正确,：程序是部分正确，同时又是终止的。,程序正确性定义（,3/3,）,（,1,）证明部分正确性的方法,A.Floyd,的不变式断言法,B.Manna,的子目标断言法,C.Hoare,的公理化方法,（,2,）终止性证明的方法,A.Floyd,的良序集方法,B.Knuth,的计数器方法,C.Manna,等人的不动点方法,（,3,）完全正确性的方法,A.Hoare,公理化方法的推广,B.,Burstall,的间发断言法,C.,Dijkstra,的弱谓词变换方法以及强验证方法,程序正确性的证明方法分类,循环不变式断言,把反映循环变量的变化规律，且在每次循环体的执行前后均为真的逻辑表达式称为该循环的,不变式断言,。,例 带余整数除法问题：设,x,为非负整数，,y,为正整数，求,x,除以,y,的商,q,，,以及余数,r,。,程序：,q,0,；,r,x,；,while(r y)/,该循环不变式断言：,/(x,yq,r)r 0,r,r,y,；,q,q,1,；,不变式断言法,证明步骤：,1,、建立断言：建立程序的输入、输出断言，如果程序中有循环出现的话，在循环中选取一个断点，在断点处建立一个循环不变式断言,2,、建立检验条件，将程序分解为不同的通路，为每一个通路建立一个检验条件，该检验条件为如下形式：,I,R=O,其中,I,为输入断言，,R,为进入通路的条件，,O,为输出断言,3,、证明检验条件：运用数学工具证明步骤,2,得到的所有检验条件，如果每一条通路检验条件都为真，则该程序为部分正确的。,不变式断言法实例,1,例：设,x,y,为正整数，求,x,y,的最大公约数,z,的程序，即,z=,gcd(x,y,),。,若,y1y2,，,gcd(y1,y2)=gcd(y1-y2,y2),若,y2y1,，,gcd(y1,y2)=gcd(y1,y2-y1),若,y1=y2,，,gcd(y1,y2)=y1=y2,不变式断言法实例,1,例：设,x,y,为正整数，求,x,y,的最大公约数,z,的程序，即,z=,gcd(x,y,),。,Function gcd(x1,x2:integer);,var,y1,y2,z:Integer;,Begin,y1:=x1;y2:=x1;,while y1y2 do,if y1y2 then,y1:=y1-y2,else y2:=y2-y1,end;,z:=y1;,write(z,);,End.,START,(x1,x2)-(y1,y2),y1y2,y1y2,y1:=y1-y2,y2:=y2-y1,z:=y1,STOP,T,F,T,F,不变式断言法实例,1,(,建立断言,),输入断言：,I(x1,x2):x10,x20,输出断言：,O(x1,x2,z):z=gcd(x1,x2),循环不变式断言,(,断点选为,b):,P(x1,x2,y1,y2):x10,x20,y10,y20,gcd(y1,y2)=gcd(x1,x2),通路划分：,通路,1,：,a-b,通路,2,：,b-d-b,通路,3,：,b-e-b,通路,4,：,b-g-c,O(x,y,z),START,(x1,x2)-(y1,y2),y1y2,y1y2,y1:=y1-y2,y2:=y2-y1,z:=y1,STOP,T,F,T,F,I(x1,x2),a,P(x1,x2,y1,y2),b,c,d,e,g,不变式断言法实例,1,(,建立检验条件,),检验条件：,I,R=O,通路,1,：,I(x1,x2)=P(x1,x2,y1,y2)(,无条件,),x10,x20,x10,x20,y10,y20,gcd(y1,y2)=gcd(x1,x2),通路,2,：,P(x1,x2,y1,y2),y1y2,y1y2=P(x1,x2,y1-y2,y2),x10,x20,y10,y20,gcd(y1,y2)=gcd(x1,x2),y1y2,y1y2,=,x10,x20,y1-y20,y20,gcd(y1-y2,y2)=gcd(x1,x2),通路,3,：,P(x1,x2,y1,y2),y1y2,y1 P(x1,x2,y1,y2-y1),通路,4,：,P(x1,x2,y1,y2),y1=y2=O(x1,x2,z),不变式断言法实例,1,(,证明检验条件,),通路,1,：无需证明,通路,2,：,前提,：,P(x1,x2,y1,y2),y1y2,y1y2=P(x1,x2,y1-y2,y2),即：,x10,x20,y10,y20,gcd(y1,y2)=gcd(x1,x2),y1y2,y1y2,结论：,x10,x20,y1-y20,y20,gcd(y1-y2,y2)=gcd(x1,x2),证明：因为,y1y2,所以,y1-y20,成立,因此有,gcd(y1-y2,y2)=gcd(y1,y2)=gcd(x1,x2),得证,通路,3:y2y1,则,gcd(y1,y2-y1)=gcd(y1,y2)=gcd(x1,x2),通路,4:z=y1=y2,则,gcd(y1,y2)=y1=y2,又因,gcd(x1,x2)=gcd(y1,y2),成立，所以,Z=gcd(x1,x2),成立,不变式断言法实例,2,对任一给定的自然数,x,，,计算,z,，,即计算,x,的平方根取整,1,3,(2n+1)=(n+1),2,(,定理,),设,y1=n;,y3=2y1+1,；,y2=(y1+1),2,;,输入断言：,I(x,):x0,输出断言：,O(x,z,):z,2,x(z+1),2,循环不变式：,P(x,y1,y2,y3),：,y1,2,(y1,y2,y3),y2+y3-y2,y2x,(y1+1,y3+2)-(y1,y3),y1-z,结束,A I(x),B P(x,y1,y2,y3),D,C O(x,z),T,F,不变式断言法实例,建立检验条件：,通路,1,：,A-B,I(x)=P(x,0,1,1),x0=0 D-B,P(x,y1,y2,y3),y2 p(x,y1+1,y2+y3+2,y3+2),y1,2,x,y2=(y1+1),2,y3=2y1+1,y2,(y1+1),2,C,P(x,y1,y2,y3),y2x=O(x,y),y1,2,x=y1,2,x(y1+1),2,不变式断言法实例,检验条件,2,y1,2,(y1+1),2,x,y2+y3+2=(y1+1+1),2,y3+1=2(y1+1)+1,证明：,x(y1+1),2,y2+y3+2=(y1+1),2,+2y1+1+2=(y1+2),2,y3+2=2y1+1+2=2(y1+1)+1,检验条件,3,y1,2,x=,y1,2,x(y1+1),2,证明：,y1,2,x,xx0,y00,输出断言：,O(x,y,z):z=,gcd(x,y,),循环不变式断言：,P(x,y):x,=0,y=0,gcd(x,y,)=gcd(x0,y0),START,Read(x,y),x0,yx,y:=y-x,x,y,z:=y,STOP,T,F,T,F,I(x,y),a,P(x,y),b,c,O(x,y,z),d,e,g,例：设,x,y,为正整数，求,x,y,的最大公约数,z,的程序，即,z=,gcd(x,y,),。,子目标断言法,(,建立断言,),输入断言,I(x,y):x00,y00,输出断言,O(x,y,z):z,=,gcd(x,y,),子目标断言,(b,为循环断点,),P(x,y,y,end,):x,=0,y=0=,y,end,=,gcd(x,y,),含义：每当控制以,x,和,y,的容许值通过,b,时，,x,和,y,的当前值的最大公约数将等于,y,的最终值,START,Read(x,y),x0,yx,y:=y-x,x,y,z:=y,STOP,T,F,T,F,I(x,y),a,P(x,y),b,c,O(x,y,z),d,e,g,子目标断言法,(,建立检验条件,),通路,1,：,b-c,检验条件,1,x=0=x=0,y=0,=,y,end,=,gcd(x,y,),通路,2,：,b-d-b,检验条件,2,P(x,y-x,y,end,),x0,yx=P(x,y,y,end,),x=0,y-x=0,y,end,=,gcd(x,y-x,),x0,y=x=,x=0,y=0,y,end,=,gcd(x,y,),通路,3,：,b-e-b,检验条件,3,P(y,x,y,end,),x0,y P(x,y,y,end,),通路,4,：,a-b,检验条件,4,x00,y00,P(x0,y0,y,end,)=,y,end,=gcd(x0,y0),子目标断言法,(,证明检验条件,),检验条件,1,：,x=0=x=0,y=0,=,y,end,=,gcd(x,y,),证明：,因为有,x=0,y,end,=y,所以,y,end,=y=gcd(0,y),=,gcd(x,y,),检验条件,2,：,P(x,y-x,y,end,),x0,yx=P(x,y,y,end,),即证明：,x=0,y-x=0,y,end,=,gcd(x,y-x,),x0,y=x=,x=0,y=0,y,end,=,gcd(x,y,),由：,x0,y=x =y0,以及,gcd(x,y-x,)=,gcd(x,y,),，可知,y,end,gcd(x,y-x,),gcd(x,y,),终止性证明的方法,Floyd,的良序集方法,Knuth,的计数器方法,程序部分正确但不终止实例,Program A,var,x,y,z,s:integer;,begin,read(x,y);,while x 0 do,if y=x then y=y x;,else x=x y;,z=y;,write(z);,end.,START,Read(x,y),x0,y=x,y:=y-x,x:=x-,y,z:=y,STOP,T,F,T,F,I(x,y),a,P(x,y),b,c,O(x,y,z),d,e,g,例：求两个正整数,x,、,y,的最大公约数,z,的程序。,可以利用不变式断言证明该程序的部分正确性，但无法证明它是终止的。,因为当,y,0,时，程序循环将不终止！,本课的内容,程序终止性证明方法：良序集方法,程序终止性证明方法：计数器方法,良序集方法证明程序终止性,1.,基本概念,偏序集,良序集,2.,采用良序集方法证明程序终止性,良序集的概念（,1/2,）,1.,偏序集,设有一个非空集合,W,和一个定义在,W,上的二元关系,，且这个关系,满足下列性质：,1,）传递性，即对于一切,a,b,c,W,如果,ab,bc,，则,ac,2,）,反对称性，即对于,a,b,则有,b,a,3,）,反自反性，即对于一切,aW,，,a,a,称,W,为具有关系,的偏序集，记做（,W,）,例如：,（,1,）具有小于关系（,）的，位于,0,1,之间的实数集合,A1,。,（,2,）,具有小于关系（,）的全体整数集合,B1,。,但将,换成 就不是,偏序集。,（,1,）具有小于关系（）的，位于,0,1,之间的实数集合,A1,。,（,2,）,具有小于关系（）的全体整数集合,B1,。,良序集的概念（,2/2,）,2.,良序集,设（,W,）,是偏序集，如果不存在由,W,中的元素构成的无限递减序列,:,a2a1a0,，,则称（,W,）,是良序集。,例如：,（,1,）若,N,是自然数集合，那么（,N,，,）,是良序集,。,（,2,）,具有通常序,A B C,Z,的字母表,=A,B,Z,是良序集。,但下述集合,A1,和,B1,是,偏序集，但不是良序集。,（,1,）具有小于关系（,）的，位于,0,1,之间的实数集合,A1,。,（,2,）,具有小于关系（,）的全体整数集合,B1,。,采用良序集证明程序终止性思路,1,、结构化程序由顺序、选择和循环三种基本结构组成，而影响程序终止性的是循环结构，因此，是程序终止性证明的重点。,2,、程序终止性证明思路：,A.,选取良序集合（,W,）；,B.,选取割点集，割断循环；,C.,在割点上寻找函数,u,使,uW,；,D.,证明每次循环，,u,依次递减。,由于良序集合（,W,）不,存在无穷递减序列，因此，循环必然终止。,用良序集方法证明程序终止性步骤,1.,选取一个点集去截断程序的各个循环部分，并在每个截断点,I,处建立中间断言,Q,i,(x,y),2.,选取一个良序集,(W,Q,j,(x,r,aj,(x,y,),证明对每一个从截断点,i,到截断点,j,的通路,aij,，,有,Q,i,(x,y),R,a i j,(x,y)=Q,j,(x,r,a i j,(x,y),即证明中间断言是“正确的”，是“良断言”,4.,证明,Q,i,(x,y)=E,i,(x,y),W,，,即终止表达式是良函数,5.,证明对于每一个从截断点,i,到截断点,j,的通路,aij,，,有,Q,i,(x,y),R,aj,(x,y)=E,j,(x,y)(y1,y2,y3),y2+y3-y2,y2,x,(y1+1,y3+2)-(y1,y3),y1-z,结束,B,T,F,良序集方法证明程序终止性实例,1.,选取断点,B,，建立中间断言,Q(x,y1,y2,y3):y2 0,2.,取良序集（,N,B,：,I(x)=Q(x,y1,y2,y3),，,即：,x0=00,从截断点,B-B,：,Q(x,y1,y2,y3),y2+y3 Q(x,y1+1,y2+y3,y3+2),即：,y20,y2+y3 y2+y30,良序集方法证明程序终止性实例,4.,证明,E(x,y),是良函数，即证明,q(x,y)=E(x,y),N,，,即,y20=x-y20,所以,x-y2,N,5.,证明终止条件成立,Q(x,y),y2+y3 E(x,y1+1,y2+y3,y3+2)E(x,y1,y2,y3),即：,y20,y2+y3 x-y2-y3=0 y=0 2x+y+I,2x0+y0,var,x,y,z,s:integer;,read(x,y);,I:=0;/,计数器赋初值,while x0 do,begin,If yx then y:=y-x;,else s:=x;x:=y;y:=s;,I:=I+1;/,计数器递增,end,z:=y;,write(z);,计数器方法证明程序终止性实例,2.,建立检验条件并证明，从而证明计数器断言为不变式断言,检验条件,1,：,a-b,x0=0 y0=0 =x0=0 y0=0 2x0+y0+0,2x0+y0,检验条件,2,：,b-d-b,x=0 y=0 (2x+y+I,2x0+y0)x0 y=x=,x=0 y-x=0 (2x+(y-x)+I+1),2x0+y0),证明：,(x-1=0),2x+(y-x)+I+1=2x+y+I-(x-1)e-b,x=0 y=0 (2x+y+I,2x0+y0)x0 y,y=0 x=0 2y+x+I+1,2x0+y0,证明：,(y0 x1=yx-1),2y+x+I+1 y+2x+I 0,。,1.2,每次循环，,N(x,y),都减小。,由,N(x,y),的值,构成一个单调递减的整数序列，,N(x,y)0,，,因而，循环只能执行有限次。,另一种计数器方法证明程序终止性实例,例：,设,x,y,为正整数，求,x,y,的最大公约数,z,的程序，即,z=,gcd(x,y,),。,选取,N(y1,y2)=max(y1,y2),容易证明：,N(y1,y2)0;,N(y1,y2),是递减的。,START,(x1,x2)-(y1,y2),y1y2,y1y2,y1:=y1-y2,y2:=y2-y1,z:=y1,STOP,T,F,T,F,采用计数器方法证明程序终止性难点,采用计数器方法证明程序终止性关键在于确定一个合适的中间断言（或选取一个合适的函数,N,（,x,y,），尤其对于一些循环次数事先难以估计的程序，要找出循环次数的上限更为困难。,作业,START,(0,，,1)-(sum,，,I),I(sum,，,I),Z=sum,STOP,T,F,1,。下图是计算,sum=X,i,的流程图程序，试证明它的部分正确性和终止性,2,。下图是判别一个整数,x2,是否为素数的流程图程序，其中,r(x,y,),表示,y,除,x,所得的余数，试证明它的部分正确性和终止性,STOP,START,y=2,yx,T,F,z=true,r(x,y,)=0,z=false,y=y+1,F,