资源描述
单击此处编辑母版标题样式,单击此处编辑母版文本样式,第二级,第三级,第四级,第五级,*,第三课,程序设计方法学基本理论 ,程序正确性证明,第三课 程序设计方法学基本理论 程序正确性证,1,什么样的程序才是正确的？,如何来保证程序是正确的？,程序正确性概述,什么样的程序才是正确的？如何来保证程序是正确的？程序正确,2,关于程序正确性的认识,根据问题的特性和软件所要实现的 功能，选择一些具有代表性的数据，设计测试用例。通过用例程序执行，去发现被测试程序的错误。,什么样的程序才是正确的？,“测试”或“调试”方法,采用“测试”方法可以发现程序中的错误，但却不能证明程序中没有错误！,因此，为保证程序的正确性，必须从理论上研究有关“程序正确性证明”的方法。,关于程序正确性的认识 根据问题的特性和软件所要,3,程序正确性证明发展历程,20世纪50年代,Turing,开始研究,1967,年，,Floyd,和,Naur,提出不变式断言法,1969年，,Hoare,提出公理化方法,1975年，,Dijkstra,提出最弱前置谓词和程序推导方法，解决了断言构造难的问题，可从程序规约推导出正确程序，使正确性证明变得实用。,程序正确性理论是十分活跃的课题，不仅可,以证明顺序程序的正确性，而且还可以证明非确,定性程序，以及并行程序的正确性。,程序正确性证明发展历程20世纪50年代 Turing开始研究,4,程序正确性理论,程序设计的一般过程,程序正确性理论 程序设计的一般过程,5,程序正确性理论,程序功能的精确描述,1、程序规约：对程序所实现功能的精确描述，,由程序的前置断言和后置断言两部分组成。,2、前置断言：程序执行前的输入应满足的条件，,又称为输入断言。,3、后置断言：程序执行后的输出应满足的条件，,又称为输出断言。,程序设计过程：问题 程序规约 程序,程序正确性理论 程序功能的精确描述 1、程序规约：对,6,程序规约的基本分类,非形式化程序规约,非形式化程序规约采用自然语言描述程序功能，简单、方便，但存在二义性，因此，不利于程序的正确性证明。,形式化程序规约,采用数学化的语言描述程序功能，描述精确，无二义性，便于程序的正确性证明。,程序规约的基本分类非形式化程序规约,7,程序规约的实例（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),程序规约的实例（1/2）在书写程序规约时，使用Q表示前置断言,8,例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）,例2：求两个非负整数的最大公约数。程序规约的实例（2/2）,9,程序正确性定义（1/3）,衡量一个程序的正确性，主要看程序是否实现了问题所要求的功能。若程序实现了问题所要求的功能，则称它为正确的，否则是不正确的。,程序设计过程：问题 程序规约 程序,对程序的正确性理解，可以分为两个层次：,从广义来说，一个程序的正确性取决于该程序满足问题实际需求的程度。,从狭义而言，如果一个程序满足了它的程序规约就是正确的。,程序正确性定义（1/3）衡量一个程序的正确性，主要看程序是否,10,程序规约,QSR,是一个逻辑表达式，其取值为真或假，其中取值为真的含义是指：给定一段程序,S，,若程序开始执行之前,Q,为真，,S,的执行将终止，且终止时,R,为真，则称为“程序,S，,关于前置断言,Q,和后置断言,R,是完全正确的”。,程序正确性定义（2/3）,程序规约QSR 是一个逻辑表达式，其取值为真或假，其中,11,部分正确,：若对于每个使得,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,是完全正确的。,一个程序的完全正确，等价于该程序是部分正确，同时又是终止的。,程序正确性定义（3/3）,部分正确：若对于每个使得Q(i)为真，并且程序S计算终止的输,12,（1）证明部分正确性的方法,A.Floyd,的不变式断言法,B.Manna,的子目标断言法,C.Hoare,的公理化方法,（2）终止性证明的方法,A.Floyd,的良序集方法,B.Knuth,的计数器方法,C.Manna,等人的不动点方法,（3）完全正确性的方法,A.Hoare,公理化方法的推广,B.Burstall,的间发断言法,C.Dijkstra,的弱谓词变换方法以及强验证方法,程序正确性的证明方法分类,（1）证明部分正确性的方法程序正确性的证明方法分类,13,循环不变式断言,把反映循环变量的变化规律，且在每次循环体的执行前后均为真的逻辑表达式称为该循环的,不变式断言,。,例 带余整数除法问题：设,x,为非负整数，,y,为正整数，求,x,除以,y,的商,q，,以及余数,r。,程序：,q0；rx；,while(r y)/,该循环不变式断言：,/(xyqr)r 0,r ry；,q q1；,循环不变式断言把反映循环变量的变化规律，且在每次循环体的执行,14,不变式断言法,证明步骤：,1、建立断言：建立程序的输入、输出断言，如果程序中有循环出现的话，在循环中选取一个断点，在断点处建立一个循环不变式断言,2、建立检验条件，将程序分解为不同的通路，为每一个通路建立一个检验条件，该检验条件为如下形式：,I,R=O,其中,I,为输入断言，,R,为进入通路的条件，,O,为输出断言,3、证明检验条件：运用数学工具证明步骤2得到的所有检验条件，如果每一条通路检验条件都为真，则该程序为部分正确的。,不变式断言法,15,不变式断言法实例,例：设,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,不变式断言法实例例：设x,y为正整数，求x,y的最大公约数z,16,不变式断言法实例,(建立断言,),输入断言：,I(x1,x2):x10,x20,输出断言：,O(x1,x2,z):z=gcd(x1,x2),循环不变式断言：,P(x1,x2,y1,y2):,x10,x20,y10 y20,gcd(y1,y2)=gcd(x1,x2),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,O(x,y,z),d,e,g,通路划分：,通路1：,a-b,通路2：,b-d-b,通路3：,b-e-b,通路4：,b-g-c,不变式断言法实例(建立断言)输入断言：START(x1,x2,17,不变式断言法实例,(建立检验条件,),检验条件：,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),不变式断言法实例(建立检验条件)检验条件：I R=,18,不变式断言法实例,(证明检验条件,),通路1：,x10,x20 x1=y1 x2=y2=,通路2：,若,y1y2.gcd(y1-y2,y2)=gcd(y1,y2)=gcd(x1,x2),通路3,若,y2y1.gcd(y1,y2)=gcd(y1,y2-y1)=gcd(x1,x2),通路4:,若,y1=y2.gcd(y1,y2)=gcd(x1,x2)=y1=y2=z,P(x1,x2,y1,y2),y1=y2=O(x1,x2,z),不变式断言法实例(证明检验条件)通路1：,19,不变式断言法实例,对任一给定的自然数,x，,计算,z ，,即计算,x,的平方根取整,13(2,n+1)=(n+1),2,y1=n;,y3=2y1+1；,y2=(y1+1),2,;,输入断言：,I(x):x0,输出断言：,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,不变式断言法实例对任一给定的自然数x，计算z ,20,不变式断言法实例,检验条件：,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,xx=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)。,不变式断言法输入断言：STARTRead(x,y)x0y,24,子目标断言法,(建立断言),输入断言,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,子目标断言法(建立断言)输入断言STARTRead(x,y)
展开阅读全文