程序正确性证明1资料讲解.ppt

单击此处编辑母版标题样式,单击此处编辑母版文本样式,第二级,第三级,第四级,第五级,3-,*,主要内容,程序正确性简介,程序测试,程序正确性证明,第5章 程序的正确性证明,内容线索,程序正确性简介,程序测试,程序正确性证明,程序的正确性,所谓一段程序是正确的，是指这段程序能准确无误地完成编写者所期望赋予它的功能。,或者说，对任何一组允许的输入信息，程序执行后能得到一组和这组输入信息相对应的正确的输出信息。,通俗地说，“做了它该做的事，没有做它不该做的事”,程序正确性的严格定义分为三种类型,部分正确性,终止性,完全正确性,如何保证程序的正确性,要求,1、从编程时就应该尽量地避免和减少错误的发生,2、当程序编好后要尽量找出错误，纠正错误,避免错误的方法,1、程序的结构要简单,2、采用标准的软件设计工具、标准的算法手册以及有效的程序设计方法,发现错误的方法,1、利用测试工具,2、利用程序的验证系统,内容线索,程序正确性简介,程序测试,程序正确性证明,程序测试,测试是程序的执行过程，目的在于发现错误。,一个好的测试用例在于能发现至今未发现的错误；,一个成功的测试是发现了至今未发现的错误的测试。,测试的原则,1.应当“尽早地和不断地进行软件测试”。,2.测试用例应由测试输入数据和对应的预期输出结果组成。,3.程序员应避免检查自己的程序。,4.在设计测试用例时，应当包括合理的输入条件和不合理的输入条件。,5.充分注意测试中的群集现象。即测试后程序中残存的错误数目与该程序中已发现的错误数目成正比。,6.严格执行测试计划，排除测试的随意性。,7.应当对每一个测试结果做全面检查。,8.妥善保存测试计划，测试用例，出错统计和最终分析报告，为维护提供方便。,程序测试的过程,程序测试的过程,程序测试的方法,两种常用的测试方法,黑盒测试,这种方法是把测试对象看做一个黑盒子，测试人员完全不考虑程序内部的逻辑结构和内部特性，只依据程序的需求规格说明书，检查程序的功能是否符合它的功能说明。,黑盒测试又叫做功能测试或数据驱动测试。,白盒测试,此方法把测试对象看做一个透明的盒子，它允许测试人员利用程序内部的逻辑结构及有关信息，设计或选择测试用例，对程序所有逻辑路径进行测试。,通过在不同点检查程序的状态，确定实际的状态是否与预期的状态一致。因此白盒测试又称为结构测试或逻辑驱动测试。,黑盒测试,黑盒测试方法是在程序接口上进行测试，主要是为了发现以下错误:,是否有不正确或遗漏了的功能?,在接口上，输入能否正确地接受?能否输出正确的结果?,是否有数据结构错误或外部信息(例如数据文件)访问错误?,性能上是否能够满足要求?,是否有初始化或终止性错误?,用黑盒测试发现程序中的错误，必须在所有可能的输入条件和输出条件中确定测试数据，来检查程序是否都能产生正确的输出。,但这是不可能的。,白盒测试,软件人员使用白盒测试方法，主要想对程序模块进行如下的检查：,对程序模块的所有独立的执行路径至少测试一次；,对所有的逻辑判定，取“真”与取“假”的两种情况都至少测试一次；,在循环的边界和运行界限内执行循环体；,测试内部数据结构的有效性等。,白盒测试,对一个具有多重选择和循环嵌套的程序，不同的路径数目可能是天文数字。给出一个小程序的流程图，它包括了一个执行20次的循环。,包含的不同执行路径数达5,20,条，对每一条路径进行测试需要1毫秒，假定一年工作365 24小时，要想把所有路径测试完，需3170年。,白盒测试,语句覆盖,判定覆盖,条件覆盖,判定条件覆盖,条件组合覆盖,路径覆盖,内容线索,程序正确性简介,程序测试,程序正确性证明,简介,Floyd不变式断言法,子目标断言法,Hoare规则公理方法,正确性证明,测试只能发现程序错误，但不能证明程序无错。,原因：测试并没有也不可能包含所有数据，只是选择了一些具有代表性的数据，所以它具有局限性。,正确性证明是通过数学技术来确定软件是否正确，也就是说，是否符合其规格说明。,正确性证明的发展,正确性证明的方法,为了证明一个程序的完全正确性，通常采用的方法是分别证明该程序的部分正确性和终止性。,主要方法有：,关于部分正确性证明的方法,Floyd的不变式断言法(,*,),Manna的子目标断言法,Hoare的公理化方法(,*,),关于终止性证明的方法,Floyd的良序集方法(,*,),Manna等人的不动点方法,Knuth的计数器方法,关于完全正确性证明的方法,Hoare的公理化方法的推广（Manna，Pnueli）,Burstall的间发断言方法,Dijkstra最弱前置谓词变换方法以及强验证方法(,*,),程序正确性理论,程序功能的精确描述,1、程序规约：对程序所实现功能的精确描述，,由程序的前置断言和后置断言两部分组成。,2、前置断言：程序执行前的输入应满足的条件，,又称为,输入,断言。,3、后置断言：程序执行后的输出应满足的条件，,又称为,输出,断言。,程序设计过程：问题 程序规约 程序,预备知识,程序的状态：程序执行到某一时刻，程序中所有变量的一组取值,初始状态：所有变量的取值使程序的前置断言为真的状态,终止状态：所有变量的取值使程序的后置断言为真的状态,程序的执行可以看作是程序状态的变迁,逻辑谓词,前提条件，初始状态,前置断言,程序，语句,结论，终止状态满足的条件,后置断言,逻辑谓词,程序规约QSR是一个逻辑表达式，其取值为真或假，其中取值为真的含义是指：给定一段程序S，若程序开始执行之前Q为真，S的执行将终止，且终止时R为真，则称为“程序S，关于前置断言Q和后置断言R是,完全正确,的”。,程序正确性定义,部分正确,：若对于每个使得Q(i)为真，并且程序S计算终止的输入信息i，R(i,S(i)都为真，则称程序S关于Q和R是部分正确的。,程序终止,：若对于每个使得Q(i)为真的输入i，程序S的计算都终止，则称程序S关于Q是终止的。,完全正确,：若对于每个使得Q(i)为真，并且程序S的计算都将终止的输入信息i，R(i,S(i)都为真，则称程序S关于Q和R是完全正确的。,一个程序的,完全正确,，等价于该程序是,部分正确,，同时又是,终止,的。,程序正确性定义,内容线索,程序正确性简介,程序测试,程序正确性证明,简介,Floyd不变式断言法,Hoare规则公理方法,Dijkstra最弱前置条件方法Dijkstra最弱前置条件方法,R.W.Floyd，1967年提出,证明一个程序的部分正确性,步骤,（1）建立断言,前置断言(,(x),)：前提条件，初始状态,后置断言(,(x,z),)：最终结论，终止状态满足的条件,循环不变式：在循环中选取一个断点，在断点处建立一个适当的断言，使循环每次执行到断点时，断言都为真,（2）建立检验条件，将程序分解为不同的通路，为每一个通路建立一个检验条件，该检验条件为如下形式：,I R=O,其中I为输入断言，R为进入通路的条件，O为输出断言,不变式断言法,（2）建立检验条件,检验条件：程序运行通过该通路时应满足的条件,i,(x,y)R,i,(x,y),i,(x,r,i,(x,y),输入断言,输出断言,y,：一组中间变量,x,：输入变量,xy：蕴含符，即,r,i,(x,y)：,通过该通路后y的值,通过此路径的条件,3、证明检验条件：运用数学工具证明步骤2得到的所有检验条件，如果每一条通路检验条件都为真，则该程序为部分正确的。,实例,设x,1,x,2,是正整数，求它们的最大公约数z=gcd(x,1,x,2,)。我们知道，对于任意正整数y,1,y,2，,有下列关系：,(1)若y,1,y,2,，gcd(y,1,y,2,)=gcd(y,1,-y,2,y,2,),(2)若y,2,y,1,，gcd(y,1,y,2,)=gcd(y,1,y,2,-y,1,),(1)若y,1,=y,2,，gcd(y,1,y,2,)=y,1,=y,2,开始,(x,1,x,2,),(y,1,y,2,),y,1,=y,2,y,1,y,2,y,1,-y,2,y,1,y,2,-y,1,y,2,A ,(x),B ,P(x,y),y,1,z,G,结束,C,(x,z),D,E,T,F,F,T,证明,(1)建立断言,(x)：,x,1,0,x,2,0,(x,z)：,z=gcd(x,1,x,2,),在B点建立不变式断言P(x,y)：,x,1,0,x,2,0,y,1,0,y,2,0,gcd(y,1,y,2,)=gcd(x,1,x,2,),(2)建立检验条件,通路1：A-B;,通路2：B-D-B,通路3：B-E-B;,通路4：B-G-C,为每一条通过，建立检验条件,开始,(x,1,x,2,),(y,1,y,2,),y,1,=y,2,y,1,y,2,y,1,-y,2,y,1,y,2,-y,1,y,2,A ,(x),B ,P(x,y),y,1,z,G,结束,C,(x,z),D,E,T,F,F,T,通路1：A-B,无条件，R,1,(x,y)恒真，结果y取值为x。,检验条件为：(x),P(x,y),即,x,1,0,x,2,0,x,1,0,x,2,0,gcd(x,1,x,2,)=gcd(x,1,x,2,),开始,(x,1,x,2,),(y,1,y,2,),y,1,=y,2,y,1,y,2,y,1,-y,2,y,1,y,2,-y,1,y,2,A ,(x),B ,P(x,y),y,1,z,G,结束,C,(x,z),D,E,T,F,F,T,证明,通路2：B-D-B,R,2,(x,y)=,y,1,y,2,y,1,y,2,r,2,(x,y),=(,y,1,-y,2,y,2,),输入输出均为P(x,y),检验条件为：,P(x,y),y,1,y,2,y,1,y,2,P(x,y,1,-y,2,y,2,),将断言P(x,y)代入，即得,x,1,0,x,2,0,y,1,0,y,2,0,gcd(y,1,y,2,)=gcd(x,1,x,2,),y,1,y,2,y,1,y,2,x,1,0,x,2,0,y,1,-y,2,0,y,2,0,gcd(y,1,-y,2,y,2,)=gcd(x,1,x,2,),开始,(x,1,x,2,),(y,1,y,2,),y,1,=y,2,y,1,y,2,y,1,-y,2,y,1,y,2,-y,1,y,2,A ,(x),B ,P(x,y),y,1,z,G,结束,C,(x,z),D,E,T,F,F,T,证明,证明,通路3：B-E-B,类似地，得到,P(x,y),y,1,y,2,y,1,y,2,P(x,y,1,y,2,-y,1,),通路4：B-G-C,类似地，得到,P(x,y),y,1,=,y,2,(x,z),开始,(x,1,x,2,),(y,1,y,2,),y,1,=y,2,y,1,y,2,y,1,-y,2,y,1,y,2,-y,1,y,2,A ,(x),B ,P(x,y),y,1,z,G,结束,C,(x,z),D,E,T,F,F,T,证明,(3)证明检验条件,通路1：,x,1,0,x,2,0,x,1,0,x,2,0,gcd(x,1,x,2,)=gcd(x,1,x,2,),显然,通路2：,x,1,0,x,2,0,y,1,0,y,2,0,gcd(y,1,y,2,)=gcd(x,1,x,2,),y,1,y,2,y,1,y,2,x,1,0,x,2,0,y,1,-y,2,0,y,2,0,gcd(y,1,-y,2,y,2,)=gcd(x,1,x,2,),检验条件前项成立时，,y,1,y,2,为真，而y,1,-y,2,0为真,且gcd(y,1,-y,2,y,2,)=gcd(y,1,y,2,)=gcd(x,1,x,2,),检验条件为真,通路3：,P(x,y),y,1,y,2,y,1,y,2,P(x,y,1,y,2,-y,1,),y,1,y,2,为真,y,1,-y,2,0,输出断言：,O(x,z):z,2,x(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,B,不变式断言法实例,检验条件：I R=O,通路1：A-B,I(x)=P(x,0,1,1),x0=0 x 1=(0+1),2,1=2*0+1,通路2：B-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,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 y2=(y1+1),2,y3=2y1+1 y2x=,y1,2,x(y1+1),2,证明：,y1,2,x,xxx,(y,1,+1,y,3,+2),(,y,1,y,3,),A ,(x),B ,P(x,y),y,1,z,结束,C,(x,z),D,T,F,y,2,+y,3,y,2,B,内容线索,程序正确性简介,程序测试,程序正确性证明,简介,Floyd不变式断言法,子目标断言法,Hoare规则公理方法,子目标断言法,子目标断言法与不变式断言法的主要区别是：,两种方法对循环所建立的断言不同。不变式断言描述了程序变量y的中间值与初始值之间关系，而子目标断言法描述的是y的中间值与循环终止时的最终值y,end,之间的关系。,两种方法进行归纳的方向不同。不变式断言沿着程序正常执行的方向进行归纳，而子目标断言法则沿着相反方向进行归纳。,不变式断言法,输入断言：,I(x,y):x0=0 y0=0,输出断言：,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,y=x,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):x0=0 y0=0,输出断言,O(x,y,z):z=gcd(x,y),子目标断言,P(x,y,y,end,):,x=0 y=0 =,y,end,=gcd(x,y),START,Read(x,y),x0,y=x,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的容许值通过L时，x,y的当前值的最大公约数等于y 的最终值。,子目标断言法,(建立检验条件),通路1：b-c 证明当控制最后一次通过L时，即控制转出循环时，子目标断言成立。,检验条件1,x=0=x=0 y=0 =y,end,=gcd(x,y),通路2：b-d-b 通过循环的then通路之后的子目标断言蕴涵通过此通路之前的子目标断言。,检验条件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 yx=x=0 y=0 y,end,=gcd(x,y),通路3：b-e-b通过循环的else通路之后的子目标断言蕴涵通过此通路之前的子目标断言。,检验条件3,P(y,x,y,end,)x0 y P(x,y,y,end,),通路4：a-b 证明如果输入断言为真，且当控制第一次通过L时子目标断言为真，则输出断言为真。,检验条件4,x0=0 y0=0 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 yx=x=0 y=0 y,end,=gcd(x,y),由：x0 yx =y0,以及 gcd(x,y-x)=gcd(x,y)，当且仅当x0,y0可知,y,end,gcd(x,y-x)gcd(x,y),内容线索,程序正确性简介,程序测试,程序正确性证明,简介,Floyd不变式断言法,子目标断言法,Hoare规则公理方法,公理化方法,公理化方法是由C.A.R.Hoare于1969年提出的一种形式化的证明程序部分正确性的方法,一、while型程序,While型程序由一个有限的语句序列组成。每个语句之间以分号隔开。B0;B1;Bn,其中B0是程序中唯一的开始语句：,START,y,f(x),Bi是下列语句之一：,（1）赋值语句：y,g(x,y),（2）条件语句：if R then F1 else F2,或者：if R do F1,（3）循环语句：while R do F1,（4）复合语句：begin F1;F2;Fk end,（5）停机语句：z,h(x,y),HALT,二、不变式演绎系统,1、不变式语句,P F Q,其中P 和Q是逻辑表达式，F是一个程序段。它的含义是：如果执行F以前P成立，且执行终止，则执行F后Q成立。这时不变式语句为,真,。不变式语句也称为,归纳表达式。,2.推理规则,A1,A2,An,B,其中B是一个不变式语句。Ai(i=1,.n)是一个逻辑表达式或者是其他的不变式语句。它的含义是：为了推论后项B为真，只需证明前项A1,A2,An为真。,为了证明不变式语句，Hoare定义了1条赋值公理和4条推理规则。,（1）赋值公理,P(x,g(x,y)y,g(x,y)P(x,y),(2)条件规则,S,1,Q和 S,2,Q,为表示方便，我们可用证明规则的一般形式,显然，上述条件语句的二种形式分别可表示为,Hoare验证系统,（3）while规则,1)while B do S,P,I,I RFI,I R=Q,P while R do FQ,P,I表示当控制进入循环时，不变式I为真；,条件I,RFI表示I是不变式，即如果执行F前I为真,且F执行终止，则F执行后I仍为真。条件I,R=Q,表示如果控制退出循环，Q将是真。,Hoare验证系统,4、并置规则,PF1R,RF2Q,PF1;F2Q,5、结论规则,P=R,RFQ,PFQ,或者,PFR R=Q,PFQ,P:true,P A0B:=AB0 B,0,P A,0B:=-AB,0,则，trueif A0 then B:=A else B=-AB,0,例：,计算X=MAX(A,B)的程序为,if A,B then X:=A else X:=B.,试验证其正确性。,证明：,P:true,P A,BX:=AX=A X,B,P AA,而 X=A X,B X=MAX(A,B),X=B XA X=MAX(A,B),故P:true if A,B then X:=A else X:=B.,X=MAX(A,B),例：,证明程序部分正确性的公理化方法就是依据以上的几条公理和规则进行的,推理过程一般有两种形式:,(1)根据给出的不变式断言,建立一些引理,根据这些引理和赋值公理,对程序P中的每一个赋值语句Fi导出相应的不变式语句Ri Fi Qi。再根据这些不变式语句和上述的四条规则逐步地组成越来越长的程序段，一直到推导出：,(x)P,(x,z)为止。这样就证明了程序P的部分正确性。,（2）从不变式语句(x)P,(x,z)出发，利用有关的规则将它逐步分解，一直到将所有的语句推演为逻辑表达式（即检验条件）。然后，证明这些逻辑表达式成立。这样就证明了程序的部分正确性。,例 利用公理化方法证明例5.2中的程序的部分正确性,START,x0,(y1,y2,y3)-(0,1,1),While y2x do,P(x,y),(y1,y2,y3)-(y1+1,y2+y3+2,y3+2),Z0=P(x,0,1,1),引理5.2 P(x,y)y2Px,y1+1,y2+y3+2,y3+2,引理5.3 P(x,y)y2x=,(x,y1),(1)根据赋值公理有,P(x,0,1,1),(y1,y2,y3)0(y1,y2,y3)-(0,1,1),P(x,y),(2)和(1)类似，根据赋值公理，引理5.2和结论规则，,P(x,y)y2x,(y1,y2,y3)x，根据while规则和（2）中的结论可得：,P(x,y),While y2x do,(y1,y2,y3)x,（4）根据并置规则和（1），（3）中的结论可得：,x0,(y1,y2,y3)-(0,1,1),While yx do,(y1,y2,y3)x,(5)根据赋值公理有：,(x,y1)zx,z0,(y1,y2,y3)-(0,1,1),While yx do,(y1,y2,y3)-(y1+1,y2+y3+2,y3+2),Z0 y00(x0,0 v,y0,0,),(x,y)x then y-y-x;,else(s,x,y)-(x,y,s),y=gcd(x0,y0),z0 y0(x0,0 v,y0,0,)gcd(x,y)=gcd(x0,y0),要证明程序A的部分正确性，只需证明下面的不变式语句：,Goal 1:,x0 y0(x0,0 v,y0,0,),Body A,y=gcd(x0,y0),第一步；根据并置规则，为了证明Goal 1，只需证明下面两个不变式语句,Goal 2,x00 y00(x0,0 v,y0,0,),（x,y）0 y0(x0,0 v,y0,0,)=P(x0,y0),根据while规则，为了证明Goal 3，只需证明,Goal 4,P(x,y)x,0,if yx then else,P(x,y),LOG 2:,P(x,y)x,=,0=,y=gcd(x0,y0),第三步：根据条件规则，为了证明Goal 4，只需证明,Goal 5：,P(x,y)x,0,yx,y-y-x,P(x,y),Goal 6:,P(x,y)x,0,yx,(s,x,y)x=P(x,y-x),LOG 4,P(x,y)x,0,yP(y,x),就将证明Goal1归结为证明逻辑表达式LOG1、LOG2、LOG3、LOG4。这四个逻辑表达式正好是例5.3中的四个检验条件，前面已经证明了他们为真。,