第六课 程序的正确性证明

第六课程序正确性证明本章主要研究内容基本概念程序测试的基本方法部分正确性证明方法终止性证明方法基本概念－程序正确性的定义一段程序是正确的，是指这段程序能正确无误地完成程序设计时所期望的功能。或者说：对任何一组允许的输入信息，程序执行后能得到一组和这组输入信息相对应的正确的输出信息。程序的正确性是衡量一个程序是否优秀的最基本条件。一段程序是错误的，是指（1）程序完成的事情并不是程序员想要完成的事情；（2）程序员想要程序完成的事情，程序并没有完成。一般来说，程序中含有错误是很难避免的。错误可能有（1）设计时的错误；（2）程序编写时的错误；（2）运行时的错误等。发现错误或尽量减少错误，是程序设计人员的努力方向，更是其职责。基本概念－程序测试如何发现错误或尽量减少错误？（1）设计程序时尽可能使用结构化程序设计方法，使程序设计过程规范化和标准化；（2）程序调试或运行时采用测试的方法去跟踪程序的运行，从而发现与改正错误；（3）利用程序正确性证明的方法检验程序是否正确。程序测试：给程序一组或几组初始值进行试运行，将运行的结果与实现已知的结果比较，若两则相同，则认为程序是正确的，若两则不同，则说明程序有错误。程序测试一个软件的开发过程要经过程序设计，设计，编写，测试与证明等一系列过程后，才能投入使用。已编写好的软件是否有错误是用户极其关心的问题。程序测试程序测试的目的是为了发现程序的错误程序测试的方法是按习惯挑选各种数据，设计测试用例程序程序测试我们测试的程序一般有两种情况：知道程序的输入和输出功能，而不知道程序的具体结构（常称为黑盒子方法）已知程序内部结构和流向，测试的用例是根据程序内部逻辑来设计的（白盒子方法）黑盒子测试方法在VAX计算机上（字长32位），输入X,Y整数，运行程序后输出Z,则输入数据可能值有2的64次方种可能。如果执行程序一次要1毫秒，那么对所有数据进行测试需要5亿年白盒子测试方法（图例）白盒子测试方法（续）一程序流程如前图所示。其中从a到b有5种路径，再外套循环20次，这样一个小程序的路径测试就有5的20次方种。如果程序执行一次从a到b平均花1分钟，整个路径需要运行2亿年才能走遍。测试用例举例例1试测试下面这一程序ProcedureP(varA,B:REAL)BeginIf(A1)and(B=0)thenX:=X/A;If(A=2)or(X1)thenX:=X+1;end测试用例举例在执行这个程序时，有各种不同的路径，如：abdabedacbdacbed测试用例举例我们可用白盒子方法设计测试用例，其任务是尽可能多地执行各种语句，以及调试到各种路径。如选择A=2,B=0,X=3则可执行路径acbed此时能覆盖到全部2个计算框，可发现一般的语句的错误我们通常把这种注重语句的复盖叫“语句复盖”测试用例举例如选择A=3,B=0,X=1A=2,B=1,X=3则可执行的路径为acbdabed从所走路径来看，上面这组数据要全面一些，它不仅通过全部两个计算框，而且第一个判别框的两边都执行过一次。我们通常把这种注重选择测试的复盖叫做“判定复盖”程序测试从以上两个例子可以看出，测试通常是不充分的，它只能发现某些错误的存在，而不能证明错误的不存在。所有，在真正设计测试用例的过程种常常要考虑经济性，可行性。测试的关键就是如何设计好高效，可行的用例程序。程序测试如选择A=2,B=0,X=4A=1,B=1,X=1则可执行的路径为acbedabd从这组数据来看，它注意了4个条件A1,B=0,A=2和X1的复盖。我们称这种注重判断的复盖为“条件复盖”程序测试以上这些数据虽然均达到一些测试目的，且各有侧重，但是都是不充分的。如从条件出发，用组合的办法使各个条件都能执行到，则我们可以写出以下8种条件组合：1)A1,B=02)A1,B0;(是不等号)3)A=1,B=04)A=1,B05)A=2,X16)A=2,X=17)A2,X18)A2,X=1程序测试根据这8种条件组合，又可以优化组成如下4组数据：A=2,B=0,X=4A=2,B=1,X=1A=1,B=0,X=2A=1,B=1,X=1它们都能使各种条件均能出现一次。虽然这个组合方法比较方便，逻辑也很清楚，且对执行条件来说还是比较全面的，但是仍然又未走遍的路径，如acbd程序测试在测试时，还要注意到计算机执行多个条件的特点，即它必须把多个条件分解为简单判别才能执行，如上述例子可分解为右图。例子2某个TRIANGLE程序，用3个整数表示一个三角形的3条边长。当输入3个整数后，该程序输出一个结果，指出这三角形是等腰，等边，还是不等边三角形。程序测试这个例子只知程序的功能，而不知内部的逻辑与结构。在选择数据组来测试程序时，我们可以凭经验，考虑如下情况：1）合理构成等腰三角形2）合理构成等边三角形3）合理构成不等边三角形4）等腰三角形的三种排列5）三个正数，其中两个数之和等于第三个数6）两边之和等于第三边的三种排列7）三个正数，其中两个数之和小于第三个数8）两边之和小于第三边的三种排列程序测试9）输入三个数，其中含有010）输入三个数，其中含有负数11）输入三个数，其中含有非整数值12）输入三个均为0的数13）输入三个均为非法字符列出各种产生的情况来测试的方法显然是黑盒子方法。它不关心盒子内程序的具体逻辑，只是根据程序功能来设计测试用例常用的测试数据选择方法有等价分类法，边缘值分析法，因果图方法和错误推测法等。程序测试等价分类法：根据程序功能将输入的数据划分为若干个等价类，然后考虑数据选择，设计出测试用例。如上例中，我们可将输入条件划分为三种三角形或划分为合理三角形，不合理三角形等二项。在选择时要同时考虑合法的和不合法的数据。有时，还要凭经验和其他知识进行更全面的测试划分。程序测试程序出错通常发生在边界状态，所以在测试中我们常常首先根据程序的功能确定边缘情况的数据变化，以便设计测试用例。对边界状态进行分析，以设计测试用例来测试程序的方法称为边缘值分析法。边缘值的选择要根据题目实际情况有针对性地，有一定创造性地进行。边缘值分析法可以考虑如下几种情况：1）恰好在边界附近，且欲越界的数据2）取最大或最小值，最多或最少值加减1的数据3）循环或迭代的初始值和终值数据4）有序集合的第一个或最后一个数据元素5）零点附近的数据6）最大误差值的数据7）文件处理时的“空文件”，“nil”，”first”等数据程序测试总之，程序测试的黑盒子方法常凭经验进行，在设计测试用例时可以综合使用上述各种方法。在设计测试数据时，我们应该考虑认为最易出错和最易忽略的地方，进行重点测试。程序测试设计测试用例的几点原则：1）测试用例的设计者最好和程序设计者不是同一个人2）对输入的数据欲输出的数据要有详细的了解与描述3）测试用例数据复盖面尽可能大4）测试时既应注意程序是否做了它预定的事，又应该注意检查它不应该做的事5）设计测试用例时要考虑经济性和可行性。程序测试美国MI公司开发的TestDirector产品作为测试管理流程平台，运用WinRunner和QuickTestProfessional作为自动化测试工具，推荐LoadRunner作为性能测试工具。MI公司作为一个跨国型业内专业公司，在自动化测试方面积累了丰富的经验。其测试工具作为目前测试市场的主流工具，市场占有率超过50％，从测试平台的先进性上来说，达到了国际上主流标准。美国SEGUE公司的SILK系列自动测试技术。SILK系列自动化黑盒测试平台能够全面适应电子商务技术的最新发展，具有测试自动化，易用易维护，场景模拟精确，支持分布式测试，支持多标准协议，扩展性强等优点。基本概念－程序正确性证明测试通常是不充分的，它只能发现某些错误的存在，而不能证明错误的不存在。为解决程序测试的不足，开展了“程序正确性证明”的方法研究。“程序正确性证明”的研究历史：（1）“程序正确性证明”开始于20世纪60年代末期，主要成就完成于70年代后期。（2）80年代OO技术的出现，对“程序正确性证明”提出了更高的要求，导致“程序正确性证明”研究日渐消退。（3）“程序正确性证明”的有关理论和技术，目前绝大多数只是使用在实验室和小规模程序功能验证中。（4）近几年来，随着UML、MDA等研究领域的出现，程序设计方法的研究焦点又逐渐回到程序的代码的自动生成上来，程序正确性证明的理论又将成为一个研究热点。基本概念－程序正确性证明程序正确性证明方法认为：一段程序的正确性是指给定一个输入断言以及程序的程序函数，能够导出程序的输出断言。输入断言：满足程序的输入条件输出断言：满足程序的输出条件严格意义上的程序正确性定义分为部分正确性、终止性和完全正确性。定义：谓词Φ(x)为输入断言，Ψ(x,z)为输出断言。（1）若对每一个使Φ(ζ)为真，并且程序计算终止的输入信息ζ、Ψ(ζ,P(ζ))为真，则称程序P关于Φ和Ψ是部分正确的。（2）若对每一个使Φ(ζ)为真，程序的计算都能终止，则称程序P对Φ是终止的。（3）若对每一个使Φ(ζ)为真的输入信息ζ，程序的计算都能终止，并且Ψ(ζ,P(ζ))为真，则称程序P关于Φ和Ψ是完全正确的。很显然，（3）等价于（1）和（2）的同时成立。基本概念－程序正确性证明程序正确性证明的基本方法（1）部分正确性证明的方法：Floyd的不变式断言法Manna的子目标断言法Hoare的公理化方法（2）终止性证明的方法Floyd的良序集方法Knuth的计数器方法Manna的不动点方法（3）完全正确性证明的方法部分正确性证明－不变式断言法不变式断言法是Floyd在1967年提出来的，是一个用于程序正确性证明的经典方法。Manna的子目标断言法和Hoare的公理化方法都是在其基础上形成的。使用不变式断言法的基本过程：（1）建立断言，建立输入断言和输出断言，如果程序中有循环，还要建立针对该循环的不变式断言，是循环执行到断点时，断言都为真。（2）建立检验条件，即程序运行通过各个通路时应该分别满足的条件。对于通路i，设其输入、输出断言分别为:Φi(x,y)、Ψ(x,y)，通过通路i的条件为:Ri(x,y),通过通路i后y的值变为ri(x,y),则检验条件为：Φi(x,y)∧Ri(x,y)－Ψi(x,ri(x,y))（3）证明检验条件，即证明（2）中所列出的所有检验条件，如果每一条通路上的检验条件都为真，则该程序是部分正确的。部分正确性证明－不变式断言法实例例1：设x1、x2是正整数，求它们的最大公约数，z=gcd(x1,x2)基本算法：对于任意正整数x1,x2，有：（1）若x1x2,gcd(x1,x2)=gcd(x1-x2,x2)（2）若x2x1,gcd(x1,x2)=gcd(x1,x2-x1)（3）若x1=x2,gcd(x1,x2)=x1=x2即反复执行（1）或（2），直到出现（3）中的情况部分正确性证明－不变式断言法实例(x1,x2)-(y1,y2)y1=y2开始y1y2y1-z结束y2-y1-y2y1-y2-y1B······P(x,y)A······Φ(x)TGC······Ψ(x,z)FEDFT部分正确性证明－不变式断言法实例利用不变式断言法实例证明该流程框图的部分正确性:(1)建立断言输入断言Φ(x):x10∧x20输出断言Ψ(x,z):z=gcd(x1,x2)考虑到存在循环，将循环在B点断开，建立B点的不变式断言：P(x,y):x10∧x20∧y10∧y20∧gcd(y1,y2)=gcd(x1,x2)其中，x,y分别表示(x1,x2)、(y1,y2)。(2)建立检验条件将B设为断点后，程序执行中所有可能的通路分解为：