《《程序正确性证明》ppt课件》由会员分享，可在线阅读，更多相关《《程序正确性证明》ppt课件（55页珍藏版）》请在金锄头文库上搜索。
1、第5章 程序正确性证明,5.1程序正确性验证概述 5.2不变式断言法 5.3子目标断言法 5.4界函数法计数器法,5.1 程序正确性概述,什么样的程序才是正确的？ 如何来保证程序是正确的？,关于程序正确性的认识,什么样的程序才是正确的？ “测试”或“调试”方法 根据问题的特性和软件所要实现的功能，选择一些具有代表性的数据，设计测试用例。通过用例程序执行，去发现被测试程序的错误。,采用“测试”方法可以发现程序中的错误，但却不能证明程序中没有错误！ 因此，为保证程序的正确性，必须从理论上研究有关“程序正确性证明”的方法。,程序正确性证明发展历程,20世纪50年代 Turing开始研究。 1967年
2、，Floyd和Naur提出不变式断言法。 1969年，Hoare提出公理化方法。 1975年，Dijkstra提出最弱前置谓词和程序推导方法，解决了断言构造难的问题，可从程序规约推导出正确程序，使正确性证明变得实用。,程序正确性理论是十分活跃的课题，不仅可 以证明顺序程序的正确性，而且还可以证明非确 定性程序，以及并行程序的正确性。,程序正确性理论,程序设计的一般过程,程序正确性理论,程序功能的精确描述 1、程序规约：对程序所实现功能的精确描述， 由程序的前置断言和后置断言两部分组成。 2、前置断言：程序执行前的输入应满足的条件， 又称为输入断言。 3、后置断言：程序执行后的输出应满足的条件，
3、 又称为输出断言。,程序规约的基本分类,非形式化程序规约 非形式化程序规约采用自然语言描述程序功能，简单、方便，但存在二义性，因此，不利于程序的正确性证明。 形式化程序规约 采用数学化的语言描述程序功能，描述精确，无二义性，便于程序的正确性证明。,程序规约的实例,在书写程序规约时，使用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 MA
4、X(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),程序正确性定义,衡量一个程序的正确性，主要看程序是否实现了问题所要求的功能。若程序实现了问题所要求的功能，则称它为正确的，否则是不正确的。 对程序的正确性理解，可以分为两个层次： 从广义来说，一个程序的正确性取决于该程序满足问题实际需求的程度。 从狭义而言，如果一个程序满足了它的程序规约就是正确的。,程序正确性定义,程序规约QSR
5、是一个逻辑表达式，其取值为真或假。 其中取值为真的含义是指：给定一段程序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)为真的输入信息i，程序S的计算都将终止，并且R(i,S(i)都为真，则称程序S关于Q和R是完全正确的。 一个程序的完全正确，等
6、价于该程序是部分正确，同时又是终止的。,程序正确性的证明方法分类,证明部分正确性的方法 A. Floyd的不变式断言法 B. Manna的子目标断言法 C. Hoare的公理化方法 终止性证明的方法 A. Floyd的良序集方法 B. Knuth的计数器方法 C.Manna等人的不动点方法 完全正确性的方法 A. Hoare公理化方法的推广 B. Burstall的间发断言法 C. Dijkstra的弱谓词变换方法以及强验证方法,第5章 程序正确性证明,5.1程序正确性验证概述 5.2不变式断言法 5.3子目标断言法 5.4界函数法计数器法,循环不变式断言,把反映循环变量的变化规律，且在每次循
7、环体的执行前后均为真的逻辑表达式称为该循环的不变式断言。,例 带余整数除法问题：设x为非负整数，y为正整数，求 x除以y的商q，以及余数r。 程序： q0；rx； while( r y) /该循环不变式断言： r ry； q q1； ,/(xyqr ) r 0,5.2 不变式断言法,证明步骤： 1、建立断言 建立程序的输入、输出断言，如果程序中有循环出现的话，在循环中选取一个断点，在断点处建立一个循环不变式断言。 2、建立检验条件 将程序分解为不同的通路，为每一个通路建立一个检验条件，该检验条件为如下形式： I R = O 其中I为输入断言，R为进入通路的条件，O为输出断言。 3、证明检验条件
8、 运用数学工具证明步骤2得到的所有检验条件，如果每一条通路检验条件都为真，则该程序为部分正确的。,不变式断言法实例1,例：设x,y为正整数，求x,y的最大公约数z的程序，即z=gcd(x,y)。,Function gcd(x1,x2:integer); var y1,y2,z : Integer; Begin y1:=x1;y2:=x2; while (y1y2) do if (y1y2) y1:=y1-y2 else y2:=y2-y1 z:=y1; write(z); End.,不变式断言法实例1(建立断言),输入断言： I(x1,x2): x10 x20 输出断言： O(x1,x2,z)
9、:z=gcd(x1,x2) 循环不变式断言： 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,不变式断言法实例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
10、(y1,y2)=gcd(x1,x2) y1y2 y1y2 = x10 x20 y1-y20 y20 gcd(y1-y2,y2)=gcd(x1,x2),不变式断言法实例1(建立检验条件),通路3： P(x1,x2,y1,y2) y1y2 y1 P(x1,x2,y1,y2-y1) x10 x20 y10 y20 gcd(y1,y2)=gcd(x1,x2) y1y2 y1 x10 x20 y10 y2-y10 gcd(y1,y2-y1)=gcd(x1,x2) 通路4： P(x1,x2,y1,y2) y1=y2 = O(x1,x2,z) x10 x20 y10 y20 gcd(y1,y2)=gcd(x
11、1,x2) y1=y2 = z=gcd(x1,x2),不变式断言法实例1(证明检验条件),通路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),不变式断言法实例2,对任一给定的自然数x，计算z ，即计算x的平方根取整。 13(2n+1)=(n+1
12、)2 y1=n; y3=2y1+1; y2= (y1+1)2 输入断言： I(x):x0 输出断言： O(x,z):z2 x(z+1)2 循环不变式： P(x,y1,y2,y3)： y12 x y2=(y1+1)2 y3 = 2y1+1,不变式断言法实例2,检验条件：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) y2x = p(x,y1+1,y2+y3+2,y3+2) y12x y2=(y1+1)2 y3 = 2y1+1 y2x = (y1+1) 2 x y2+y3+2=(y
13、1+1+1) 2 y3+2=2(y1+1)+1 通路3：B-C P(x,y1,y2,y3) y2x =O(x,y1) y12 x y2=(y1+1)2 y3 = 2y1+1 y2x = y12 x(y1+1)2,不变式断言法实例2,检验条件2 y12 x y2=(y1+1)2 y3 = 2y1+1 y2 x = (y1+1) 2 x y2+y3+2=(y1+1+1) 2 y3+2=2(y1+1)+1 证明： x(y1+1)2 (y2 x , y2=(y1+1)2 ) y2+y3+2 = (y1+1)2 + 2y1 + 1+2 = (y1+1)2 +2 (y1+1)+1= (y1+1+1)2 y
14、3+2=2y1+1+2=2(y1+1)+1 检验条件3 y12 x y2=(y1+1)2 y3 = 2y1+1 y2x = y12 xx(y1+1)2,作业,课本P174习题1、习题2。要求用不变式断言法证明。,第5章 程序正确性证明,5.1程序正确性验证概述 5.2不变式断言法 5.3子目标断言法 5.4界函数法计数器法,5.3子目标断言法,子目标断言法与不变式断言法的主要区别是： 两种方法对循环所建立的断言不同。 不变式断言描述了程序变量y的中间值与初始值之间关系； 子目标断言法描述的是y的中间值与循环终止时的最终值yend之间的关系。 两种方法进行归纳的方向不同。 不变式断言沿着程序正常
15、执行的方向进行归纳； 子目标断言法则沿着相反方向进行归纳。,不变式断言法,输入断言： 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),例：设x,y为非负整数，求x,y的最大公约数z的程序，即z=gcd(x,y)。,子目标断言法(建立断言),输入断言 I(x,y): x0 =0 y0 =0 (x00 y00) 输出断言 O(x,y,z): z=gcd(x,y) 子目标断言 P(x,y,yend): x=0 y=0 (x0 y0) = yend = 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, yend),b,c,O(x,y,z),d,e,g,子目标断言法(建立检验条件),通路1： 控制转出循环时，子目标断言成立。 通路2、通路3： 如果在通过循环之后，子目标断言在断点处成立，那么
