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