程序正确性证明课件

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

1、主要内容,程序正确性简介 程序测试 程序正确性证明,第5章 程序的正确性证明,内容线索,程序正确性简介 程序测试 程序正确性证明,程序的正确性,所谓一段程序是正确的，是指这段程序能准确无误地完成编写者所期望赋予它的功能。 或者说，对任何一组允许的输入信息，程序执行后能得到一组和这组输入信息相对应的正确的输出信息。 通俗地说，“做了它该做的事，没有做它不该做的事” 程序正确性的严格定义分为三种类型 部分正确性 终止性 完全正确性,如何保证程序的正确性,要求 1、从编程时就应该尽量地避免和减少错误的发生 2、当程序编好后要尽量找出错误，纠正错误 避免错误的方法 1、程序的结构要简单 2、采用标准的

2、软件设计工具、标准的算法手册以及有效的程序设计方法 发现错误的方法 1、利用测试工具 2、利用程序的验证系统,内容线索,程序正确性简介 程序测试 程序正确性证明,程序测试,测试是程序的执行过程，目的在于发现错误。 一个好的测试用例在于能发现至今未发现的错误； 一个成功的测试是发现了至今未发现的错误的测试。 测试的原则 1. 应当 “尽早地和不断地进行软件测试” 。 2. 测试用例应由测试输入数据和对应的预期输出结果组成。 3. 程序员应避免检查自己的程序。 4. 在设计测试用例时，应当包括合理的输入条件和不合理的输入条件。 5. 充分注意测试中的群集现象。即测试后程序中残存的错误数目与该程序中

3、已发现的错误数目成正比。 6. 严格执行测试计划，排除测试的随意性。 7. 应当对每一个测试结果做全面检查。 8. 妥善保存测试计划，测试用例，出错统计和最终分析报告，为维护提供方便。,程序测试的过程,程序测试的过程,程序测试的方法,两种常用的测试方法 黑盒测试 这种方法是把测试对象看做一个黑盒子，测试人员完全不考虑程序内部的逻辑结构和内部特性，只依据程序的需求规格说明书，检查程序的功能是否符合它的功能说明。 黑盒测试又叫做功能测试或数据驱动测试。 白盒测试 此方法把测试对象看做一个透明的盒子，它允许测试人员利用程序内部的逻辑结构及有关信息，设计或选择测试用例，对程序所有逻辑路径进行测试。 通

4、过在不同点检查程序的状态，确定实际的状态是否与预期的状态一致。因此白盒测试又称为结构测试或逻辑驱动测试。,黑盒测试,黑盒测试方法是在程序接口上进行测试，主要是为了发现以下错误: 是否有不正确或遗漏了的功能? 在接口上，输入能否正确地接受? 能否输出正确的结果? 是否有数据结构错误或外部信息(例如数据文件)访问错误? 性能上是否能够满足要求? 是否有初始化或终止性错误? 用黑盒测试发现程序中的错误，必须在所有可能的输入条件和输出条件中确定测试数据，来检查程序是否都能产生正确的输出。 但这是不可能的。,白盒测试,软件人员使用白盒测试方法，主要想对程序模块进行如下的检查： 对程序模块的所有独立的执行

5、路径至少测试一次； 对所有的逻辑判定，取“真”与取“假”的两种情况都至少测试一次； 在循环的边界和运行界限内执行循环体； 测试内部数据结构的有效性等。,白盒测试,对一个具有多重选择和循环嵌套的程序，不同的路径数目可能是天文数字。给出一个小程序的流程图，它包括了一个执行20次的循环。 包含的不同执行路径数达520条，对每一条路径进行测试需要1毫秒，假定一年工作365 24小时，要想把所有路径测试完，需3170年。,白盒测试,语句覆盖 判定覆盖 条件覆盖 判定条件覆盖 条件组合覆盖 路径覆盖,内容线索,程序正确性简介 程序测试 程序正确性证明 简介 Floyd不变式断言法 子目标断言法 Hoare

6、规则公理方法,正确性证明,测试只能发现程序错误，但不能证明程序无错。 原因：测试并没有也不可能包含所有数据，只是选择了一些具有代表性的数据，所以它具有局限性。 正确性证明是通过数学技术来确定软件是否正确，也就是说，是否符合其规格说明。,正确性证明的发展,正确性证明的方法,为了证明一个程序的完全正确性，通常采用的方法是分别证明该程序的部分正确性和终止性。 主要方法有： 关于部分正确性证明的方法 Floyd的不变式断言法(*) Manna的子目标断言法 Hoare的公理化方法(*) 关于终止性证明的方法 Floyd的良序集方法(*) Manna等人的不动点方法 Knuth的计数器方法 关于完全正确

7、性证明的方法 Hoare的公理化方法的推广（ Manna ，Pnueli） Burstall的间发断言方法 Dijkstra最弱前置谓词变换方法以及强验证方法(*),程序正确性理论,程序功能的精确描述,1、程序规约：对程序所实现功能的精确描述， 由程序的前置断言和后置断言两部分组成。 2、前置断言：程序执行前的输入应满足的条件， 又称为输入断言。 3、后置断言：程序执行后的输出应满足的条件， 又称为输出断言。,预备知识,程序的状态：程序执行到某一时刻，程序中所有变量的一组取值 初始状态：所有变量的取值使程序的前置断言为真的状态 终止状态：所有变量的取值使程序的后置断言为真的状态 程序的执行可以

8、看作是程序状态的变迁,程序规约QSR是一个逻辑表达式，其取值为真或假，其中取值为真的含义是指：给定一段程序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)为真，并且程序S的计算都将终止的输入信息i，R(i,S(i)都为真，则称程序S关于Q和R是完全正确

9、的。 一个程序的完全正确，等价于该程序是部分正确，同时又是终止的。,程序正确性定义,内容线索,程序正确性简介 程序测试 程序正确性证明 简介 Floyd不变式断言法 Hoare规则公理方法 Dijkstra最弱前置条件方法Dijkstra最弱前置条件方法,R.W.Floyd，1967年提出 证明一个程序的部分正确性 步骤 （1）建立断言 前置断言(x)：前提条件，初始状态 后置断言(x,z)：最终结论，终止状态满足的条件 循环不变式：在循环中选取一个断点，在断点处建立一个适当的断言，使循环每次执行到断点时，断言都为真 （2）建立检验条件，将程序分解为不同的通路，为每一个通路建立一个检验条件，该

10、检验条件为如下形式： I R = O,其中I为输入断言，R为进入通路的条件，O为输出断言,不变式断言法,（2）建立检验条件 检验条件：程序运行通过该通路时应满足的条件,i(x,y) Ri(x,y) i(x,r i(x,y),输入断言,输出断言,y： 一组中间变量 x：输入变量 xy：蕴含符，即 ri(x,y)：通过该通路后y的值,通过此路径的条件,3、证明检验条件：运用数学工具证明步骤2得到的所有检验条件，如果每一条通路检验条件都为真，则该程序为部分正确的。,实例,设x1,x2是正整数，求它们的最大公约数z=gcd(x1,x2)。我们知道，对于任意正整数y1,y2，有下列关系：,(1) 若y1

11、y2， gcd(y1,y2)= gcd(y1- y2,y2) (2) 若y2y1， gcd(y1,y2)= gcd(y1,y2 - y1) (1) 若y1=y2， gcd(y1,y2)= y1=y2,开始,(x1,x2) (y1,y2),y1=y2,y1y2,y1-y2 y1,y2-y1 y2,A (x),B P(x,y),y1 z,G,结束,C (x,z),D,E,T,F,F,T,证明,(1)建立断言 (x)： x10 x2 0 (x,z)： z=gcd(x1,x2) 在B点建立不变式断言P(x,y)： x10 x2 0 y10 y2 0 gcd(y1,y2)= gcd(x1,x2) (2)

12、建立检验条件 通路1：A-B; 通路2：B-D-B 通路3：B-E-B; 通路4：B-G-C 为每一条通过，建立检验条件,通路1：A-B 无条件， R1(x,y)恒真，结果y取值为x。 检验条件为： (x) P(x,y) 即 x10 x2 0 x10 x2 0 gcd(x1,x2)= gcd(x1,x2),证明,通路2：B-D-B R2(x,y)=y1y2 y1y2 r2(x,y) =(y1- y2,y2) 输入输出均为P(x,y) 检验条件为： P(x,y) y1y2 y1y2 P(x, y1- y2,y2) 将断言P(x,y)代入，即得 x10 x2 0 y10 y2 0 gcd(y1,y

13、2)= gcd(x1,x2) y1y2 y1y2 x10 x2 0 y1 - y2 0 y2 0 gcd(y1 - y2,y2)= gcd(x1,x2),证明,证明,通路3： B-E-B 类似地，得到P(x,y) y1y2 y1y2 P(x, y1,y2 - y1) 通路4： B-G-C 类似地，得到P(x,y) y1=y2 (x,z),证明,(3) 证明检验条件 通路1：x10 x2 0 x10 x2 0 gcd(x1,x2)= gcd(x1,x2) 显然 通路2： x10 x2 0 y10 y2 0 gcd(y1,y2)= gcd(x1,x2) y1y2 y1y2 x10 x2 0 y1

14、- y2 0 y2 0 gcd(y1 - y2,y2)= gcd(x1,x2) 检验条件前项成立时， y1y2 为真，而y1 - y2 0为真 且gcd(y1 - y2,y2) = gcd(y1,y2) = gcd(x1,x2) 检验条件为真 通路3： P(x,y) y1y2 y1y2 P(x, y1,y2 - y1) y1y2为真, y1- y2 0为真, gcd(y1,y2 - y1) = gcd(y1,y2) = gcd(x1,x2) 检验条件为真 通路4：P(x,y) y1=y2 (x,z) y1=y2,gcd(y1,y2) = y1 = y2 ,检验条件为真,不变式断言法实例,对任一

15、给定的自然数x，计算z ， 即计算x的平方根取整 算法：13(2n+1)=(n+1)2 取： y1=n; y3=奇数2n+1； y2=1+3+5+(2n+1)= (n+1) 2 =(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,A I(x),B P(x,y1,y2,y3),D,C O(x,z),T,F,B,不变式断言法实例,检验条件：I R = O 通路1：A-B I(x)= P(x,0,1,1) x0= 0 x 1=(0+1) 2 1=2*0+1

16、 通路2：B-D-B P(x,y1,y2,y3) y2 p(x,y1+1,y2+y3+2,y3+2) y12 (y1+1) 2 C P(x,y1,y2,y3) y2x =O(x,y) y12x = y12x(y1+1)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+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 y12 x y2=(y1+1)2 y3 = 2y1+1 y2x = y12 xx(y1+1)2,同步练