第5章程序正确性证明ppt课件

1、第5章 程序正确性证明5.1程序正确性验证概述5.2不变式断言法5.3子目的断言法5.4界函数法计数器法 5.1 程序正确性概述什么样的程序才是正确的？如何来保证程序是正确的？themegallery计算机程序是算法的一种准确描画，算法的义务是把给定的输入信息变换为所需求的输出信息。所谓一段程序是正确的，是指这段程序能准确无误地完成编写者所期望赋予它的功能。或者说，对任何一组允许的输入信息，程序执行后能得到一组和这组输入信息相对应的正确的输出信息。通俗地说，“做了它该做的事，没有做它不该做的事。构造化程序的正确性验证themegallery一段程序是错误的，是指：(1)程序完成的事情并不是程序

2、员想要完成的事情；(2)程序员想要程序完成的事情，程序并没有完成。普通来说，程序中含有错误是很难防止的错误能够有：1设计时的错误；2程序编写时的错误；3运转时的错误等;themegallery如何发现错误或尽量减少错误？(1)设计程序时尽能够运用构造化程序设计方法，使程序设计过程规范化和规范化；(2)程序调试或运转时采用测试的方法去跟踪程序的运转，从而发现与矫正错误；(3)利用程序正确性证明的方法检验程序能否正确。themegallery1983年IEEE提出的软件工程术语中给软件测试下的定义是：“运用人工或者自动手段来运转或测定某个系统的过程，其目的在于检验它能否满足规定的需求或是弄清预期结

3、果与实践结果之间的差别。测试是程序的执行过程，目的在于发现错误。一个好的测试用例在于能发现至今未发现的错误； 一个胜利的测试是发现了至今未发现的错误的测试。themegallery测试的原那么1. 该当 “尽早地和不断地进展软件测试 。2. 测试用例应由测试输入数据和对应的预期输出结果组成。3. 程序员应防止检查本人的程序。4. 在设计测试用例时，该当包括合理的输入条件和不合理的输入条件。themegallery5. 充分留意测试中的群集景象。即测试后程序中残存的错误数目与该程序中已发现的错误数目成正比。6. 严厉执行测试方案，排除测试的随意性。7. 该当对每一个测试结果做全面检查。8. 妥善

4、保管测试方案，测试用例，出错统计和最终分析报告，为维护提供方便。themegallery程序测试本质上只是一种抽样检查测试过程： 选取测试数据 执行程序 输入测试数据 记录执行结果 手工核对结果 因此，测试只是一种查错的手段，它可以协助人们去发现程序中的错误，但不能证明程序中没有错误，即：测试不能证明程序是正确的 themegallery测试只能发现程序错误，但不能证明程序无错。 缘由：测试并没有也不能够包含一切数据，只是选择了一些具有代表性的数据，所以它具有局限性。正确性证明是经过数学技术来确定软件能否正确，也就是说，能否符合其规格阐明。关于程序正确性的认识什么样的程序才是正确的？ “测试或

5、“调试方法根据问题的特性和软件所要实现的功能，选择一些具有代表性的数据，设计测试用例。经过用例程序执行，去发现被测试程序的错误。 采用“测试方法可以发现程序中的错误，但却不能证明程序中没有错误！ 因此，为保证程序的正确性，必需从实际上研讨有关“程序正确性证明的方法。程序正确性证明开展历程20世纪50年代 Turing开场研讨。1967年，Floyd和Naur提出不变式断言法。1969年，Hoare提出公理化方法。1975年，Dijkstra提出最弱前置谓词和程序推导方法，处理了断言构造难的问题，可从程序规约推导出正确程序，使正确性证明变得适用。 程序正确性实际是非常活泼的课题，不仅可以证明顺序

6、程序的正确性，而且还可以证明非确定性程序，以及并行程序的正确性。程序正确性实际程序设计的普经过程程序正确性实际程序功能的准确描画1、程序规约：对程序所实现功能的准确描画， 由程序的前置断言和后置断言两部分组成。2、前置断言：程序执行前的输入应满足的条件， 又称为输入断言。3、后置断言：程序执行后的输出应满足的条件， 又称为输出断言。 程序设计过程：问题 程序规约 程序程序规约的根本分类非方式化程序规约 非方式化程序规约采用自然言语描画程序功能，简单、方便，但存在二义性，因此，不利于程序的正确性证明。方式化程序规约 采用数学化的言语描画程序功能，描画准确，无二义性，便于程序的正确性证明。程序规约

7、的实例在书写程序规约时，运用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

8、)程序正确性定义衡量一个程序的正确性，主要看程序能否实现了问题所要求的功能。假设程序实现了问题所要求的功能，那么称它为正确的，否那么是不正确的。对程序的正确性了解，可以分为两个层次：从广义来说，一个程序的正确性取决于该程序满足问题实践需求的程度。从狭义而言，假设一个程序满足了它的程序规约就是正确的。程序设计过程：问题 程序规约 程序程序正确性定义程序规约QSR是一个逻辑表达式，其取值为真或假。其中取值为真的含义是指：给定一段程序S，假设程序开场执行之前Q为真，S的执行将终止，且终止时R为真，那么称为 “程序S，关于前置断言Q和后置断言R是完全正确的。程序正确性定义部分正确：假设对于每个使得Q(

9、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是完全正确的。一个程序的完全正确，等价于该程序是部分正确，同时又是终止的。程序正确性的证明方法分类证明部分正确性的方法 A. Floyd的不变式断言法 B. Manna的子目的断言法 C. Hoare的公理化方法终止性证明的方法 A. Floyd的良序集方法 B. Knuth的

10、计数器方法 C.Manna等人的不动点方法完全正确性的方法 A. Hoare公理化方法的推行 B. Burstall的间发断言法 C. Dijkstra的弱谓词变换方法以及强验证方法第5章 程序正确性证明5.1程序正确性验证概述5.2不变式断言法5.3子目的断言法5.4界函数法计数器法循环不变式断言把反映循环变量的变化规律，且在每次循环体的执行前后均为真的逻辑表达式称为该循环的不变式断言。 例 带余整数除法问题：设x为非负整数，y为正整数，求 x除以y的商q，以及余数r。 程序： q0；rx； while( r y) /该循环不变式断言： r ry； q q1； /(xyqr ) r 05.2

11、 不变式断言法证明步骤：1、建立断言建立程序的输入、输出断言，假设程序中有循环出现的话，在循环中选取一个断点，在断点处建立一个循环不变式断言。2、建立检验条件将程序分解为不同的通路，为每一个通路建立一个检验条件，该检验条件为如下方式：I R = O 其中I为输入断言，R为进入通路的条件，O为输出断言。3、证明检验条件运用数学工具证明步骤2得到的一切检验条件，假设每一条通路检验条件都为真，那么该程序为部分正确的。不变式断言法实例1例：设x,y为正整数，求x,y的最大公约数z的程序，即z=gcd(x,y)。Function gcd(x1,x2:integer);var y1,y2,z : Inte

12、ger;Beginy1:=x1;y2:=x2;while (y1y2) do if (y1y2) y1:=y1-y2 else y2:=y2-y1 z:=y1; write(z); End.START(x1,x2)(y1,y2)y1y2y1y2y1:=y1-y2y2:=y2-y1z:=y1STOPTFTF不变式断言法实例1(建立断言)输入断言：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) 通路划分：通路1：a-b通路2：b-d-b

13、通路3：b-e-b通路4：b-g-cSTART(x1,x2)-(y1,y2)y1y2y1y2y1:=y1-y2y2:=y2-y1z:=y1STOPTFTFI(x1,x2)aP(x1,x2,y1,y2)bcO(x1,x2,z)deg不变式断言法实例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(x

14、1,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 y1x10 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(x1,x2) y1=y2 = z=gcd(x1

15、,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)2 y1=n; y3=2y1+1; y2= (y1+1)2

16、输入断言： I(x):x0输出断言： O(x,z):z2 x(y1,y2,y3)y2+y3y2y 2 x(y1+1,y3+2)(y1,y3)y1z终了A I(x)B P(x,y1,y2,y3)DC O(x,z)FT不变式断言法实例2检验条件：I R = O通路1：A-BI(x)= P(x,0,1,1)x0= 0 x 1=(0+1) 2 1=2*0+1通路2：B-D-BP(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=(y1+1+1) 2 y3+2=2(y1+

17、1)+1通路3：B-CP(x,y1,y2,y3) y2x =O(x,y1)y12 x y2=(y1+1)2 y3 = 2y1+1 y2x = y12 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 y3+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

18、 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)例：设x,y为非负整数，求x,y的最大公约数z的程序，即z=gcd(x,y)。STARTRead(x,y)x0y=xy:=y-xx yz:=ySTOPTFTFI(x,y)aP(x,y)bcO(x,y,z)deg子目的断言法(建立断言)输入断言 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 =

19、gcd(x,y)STARTRead(x,y)x0y=xy:=y-xx yz:=ySTOPTFTFI(x,y)aP(x,y, yend)bcO(x,y,z)deg子目的断言法(建立检验条件)通路1：控制转出循环时，子目的断言成立。通路2、通路3：假设在经过循环之后，子目的断言在断点处成立，那么，在经过循环之前，断言也成立。通路4：假设输入断言为真，且控制第一次经过断点B时子目的断言为真，那么输出断言为真。子目的断言法(建立检验条件)通路1：b-c 检验条件1 x=0 = P(x,y,yend)x=0 = x=0 y=0 (x0 y0) = yend =gcd(x,y) 通路2：b-d-b 检验条

20、件2P(x,y-x, yend) x0 y=x =P(x,y, yend) x=0 y-x=0 (x0 y-x0) = yend = gcd(x,y-x) x0 y=x = x=0 y=0 (x0 y0) = 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 (x0 0 y0 0) P(x0, y0, yend)= yend = gcd(x0, y0)子目的断言法(证明检验条件)检验条件1：x=0 = x=0 y=0 = yend =gcd(x,y)证明：由于有 x=0,

21、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 (x0 y-x0) = yend = gcd(x,y-x) x0 y=x = x=0 y=0 (x0 y0) = yend = gcd(x,y) 程序部分正确但不终止实例例：求两个非负整数x、y的最大公约数z的程序。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

22、= y; write (z); end. STARTRead(x,y)x0yxy:=y-xx :=x-yz:=ySTOPTFTFI(x,y)aP(x,y)bcO(x,y,z)deg 可以利用不变式断言等方法证明该程序的部分正确性，但无法证明它是终止的。 由于当y0时，程序循环将不终止！ 第5章 程序正确性证明5.1程序正确性验证概述5.2不变式断言法5.3子目的断言法5.4界函数法计数器法5.4计数器方法证明程序终止性证明思绪经过估计循环执行的最大次数证明程序终止性的方法。证明步骤:1.为程序的每一个循环附加一个新的变量作为该循环的计数器，初始值置为0，每循环一次该计数器加1。2.为每个循环设

23、置一个中延续言，它表示相应的计数器不会超越固定的界限。3.证明2中的中延续言是不变式断言。计数器方法证明程序终止性实例计算非负整数的最大公约数var x,y,z,s: integer;begin Read(x,y) while x0 do begin If yx then y:=y-x; else s:=x;x:=y;y:=s;endz:=y;write(z);endSTARTRead(x,y)x0y xy:=y-xx yz:=ySTOPTFTFI(x,y)aP(x,y)bO(x,y)dec计数器方法证明程序终止性实例1.引进计数器I,并建立如下断言 x0 y 0 2x+y+I 2x0+y0

24、var x,y,z,s: integer;read(x,y);I:=0; /计数器赋初值while x0 dobegin if y x then y:=y-x; else s:=x;x:=y;y:=s fi; I:= I+1; /计数器递增End;z:=y;write(z);计数器方法证明程序终止性实例2.建立检验条件并证明，从而证明计数器断言为不变式断言。检验条件1：a - bx00y00 = x00y002x0+y0+02x0+y0检验条件2：b - d - bx0y0(2x+y+I2x0+y0)x0yx =x0y-x0(2x+(y-x)+I+12x0+y0)证明： x0 = (x-10)

25、 2x+(y-x)+I+1=2x+y+I-(x-1) 2x+y+I 2x0+y0检验条件3：b - e - bx0y0(2x+y+I2x0+y0)x0yy0 x0(2y+x+I+1 2x0+y0) 证明： (y yx-1) 2y+x+I+1y+x-1+x+I+1=y+2x+I 2x0+y0 由于2x+y+I2x0+y0是不变式断言，因此，I循环次数必定小于常量2x0+y0 ，也就是循环只能执行有限次，即程序终止。 采用计数器方法证明程序终止性和利用不变式断言法证明部分正确性步骤完全类似，只需再添加输出断言部分检验条件并证明，即可完成程序部分正确性证明。 因此，可以把上述两者结合起来，完成程序的完全正确性证明。 5.4 界函数法计数器方法的变形该方法是计数器方法的一种变形，证明程序的可终止性的常用方法.界函数法:对程序中的每一个循环,构造一个界函数,假设该循环存在界函数,那么该循环是可终止的,否那么,该循环不可终止.界函数必需满足的条件: (1)与循环变量有关的整函数,记为N(x,y); (2)在循环的过程中N(x,y)0; (3)每执行一次循环, N(x,y)的值减小.3