程序正确性证明概述

《程序正确性证明概述》由会员分享，可在线阅读，更多相关《程序正确性证明概述（54页珍藏版）》请在金锄头文库上搜索。

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

2、 (2)程序员想要程序完成的事情，程序并没有完成。 一般来说，程序中含有错误是很难避免的错误 可能有： （1）设计时的错误； （2）程序编写时的错误； （3）运行时的错误等; ,,如何发现错误或尽量减少错误？ (1)设计程序时尽可能使用结构化程序设计方法，使 程序设计过程规范化和标准化； (2)程序调试或运行时采用测试的方法去跟踪程序的 运行，从而发现与改正错误； (3)利用程序正确性证明的方法检验程序是否正确。,,1983年IEEE提出的软件工程术语中给软件测试下的定义是：“使用人工或者自动手段来运行或测定某个系统的过程，其目的在于检验它是否满足规定的需求或是弄清预期结果与实际结果之间的差别

3、。” 测试是程序的执行过程，目的在于发现错误。 一个好的测试用例在于能发现至今未发现的错误； 一个成功的测试是发现了至今未发现的错误的测试。,,测试的原则,1. 应当 “尽早地和不断地进行软件测试” 。 2. 测试用例应由测试输入数据和对应的预期输出结果组成。 3. 程序员应避免检查自己的程序。 4. 在设计测试用例时，应当包括合理的输入条件和不合理的输入条件。,,5. 充分注意测试中的群集现象。即测试后程序中残存的错误数目与该程序中已发现的错误数目成正比。 6. 严格执行测试计划，排除测试的随意性。 7. 应当对每一个测试结果做全面检查。 8. 妥善保存测试计划，测试用例，出错统计和最终分析

4、报告，为维护提供方便。,,程序测试实质上只是一种抽样检查 测试过程： 选取测试数据 执行程序 输入测试数据 记录执行结果 手工核对结果 因此，测试只是一种查错的手段，它可以帮助人们去发现程序中的错误，但不能证明程序中没有错误，即：测试不能证明程序是正确的,,测试只能发现程序错误，但不能证明程序无错。 原因：测试并没有也不可能包含所有数据，只是选择了一些具有代表性的数据，所以它具有局限性。 正确性证明是通过数学技术来确定软件是否正确，也就是说，是否符合其规格说明。,关于程序正确性的认识,什么样的程序才是正确的？ “测试”或“调试”方法 根据问题的特性和软件所要实现的功能，选择一些具有代表性的数据

5、，设计测试用例。通过用例程序执行，去发现被测试程序的错误。,采用“测试”方法可以发现程序中的错误，但却不能证明程序中没有错误！ 因此，为保证程序的正确性，必须从理论上研究有关“程序正确性证明”的方法。,程序正确性证明发展历程,20世纪50年代 Turing开始研究。 1967年，Floyd和Naur提出不变式断言法。 1969年，Hoare提出公理化方法。 1975年，Dijkstra提出最弱前置谓词和程序推导方法，解决了断言构造难的问题，可从程序规约推导出正确程序，使正确性证明变得实用。,程序正确性理论是十分活跃的课题，不仅可 以证明顺序程序的正确性，而且还可以证明非确 定性程序，以及并行程

6、序的正确性。,程序正确性理论,程序设计的一般过程,程序正确性理论,程序功能的精确描述 1、程序规约：对程序所实现功能的精确描述， 由程序的前置断言和后置断言两部分组成。 2、前置断言：程序执行前的输入应满足的条件， 又称为输入断言。 3、后置断言：程序执行后的输出应满足的条件， 又称为输出断言。,程序规约的基本分类,非形式化程序规约 非形式化程序规约采用自然语言描述程序功能，简单、方便，但存在二义性，因此，不利于程序的正确性证明。 形式化程序规约 采用数学化的语言描述程序功能，描述精确，无二义性，便于程序的正确性证明。,程序规约的实例,在书写程序规约时，使用Q表示前置断言，R表示后置断言，S表

7、示问题求解的实现程序。在前置断言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(i)为真，并且程序S计算终止的输入信息i，R(i,S(i)都为真，则称程序S关于

9、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的计数器方法 C.Manna等人的不动点方法 完全正确性的方法 A. Hoa

10、re公理化方法的推广 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 0,5.2 不变式断言法,证明步骤： 1、建立断言 建立程序的输

11、入、输出断言，如果程序中有循环出现的话，在循环中选取一个断点，在断点处建立一个循环不变式断言。 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 : Integer; Begin y1:=x

12、1;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):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(x

13、1,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),不变式断言法实例1(建立检验条件),通路3： P(x1,x2,y1,y2) y1y2 y1 P(x1,x2,y1,y2-y1) x10 x20 y10 y20 gcd(y1

14、,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(x1,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) =

15、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 输入断言： 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 =