软件验证技术..PPT课件

1、1,第7章 软件验证技术(第7.9-7.10节）,2,主要内容,程序正确性证明 调试,3,7.9 程序正确性证明,测试可以帮助人们发现程序中的错误，但它却不能证明程序中没有错误。 早在50年代，图林（Turing）等人就开始注意并开展了程序正确性证明这方面的早期研究工作；60年代后半期，Floyd和Hoare等人提出了不变式断言法和公理化方法，使得这一研究进入了一个蓬勃发展的新阶段；在此之后，出现了许多不同的程序正确性证明方法。,4,7.9.1 程序正确性定义,所谓一段程序是正确的，是指这段程序能准确无误地完成预定的功能。或者说，对任何一组允许的输入，程序执行后能得到一组相应的正确的输出。 在

2、研究程序正确性证明时，将一段程序的输入和输出应满足的条件的逻辑关系式分别称为此段程序的输入断言（或初始断言、前置断言）和输出断言（或结果断言、后置断言），通常用谓词(x)和(x，z)表示，其中x和z分别表示输入和输出数据（可以是一个或一组变量）。,5,例子,unsigned power(unsigned x,unsigned y) unsigned z; z=1; while (x!=0) z=z*y; x=x-1; return z; 则 (x,y):x0, y0； (x,y,z):z=yx。,6,程序正确性三种类型,程序的部分正确性 程序的终止性 程序的完全正确性,7,程序的部分正确性,若

3、每一个使得（x）为真且程序计算终止的输入数据x，（x，p（x）都为真，则称程序p关于和是部分正确的。 这里p（x）表示与输入数据x相对应的程序p的输出数据。,8,程序的终止性,若每一个使得（x）为真的输入数据x，程序计算都终止，则称程序P对是终止的。,9,程序的完全正确性,若每一个使得（x）为真的输入数据x，程序计算都终止且（x，P（x）为真，则称程序P关于和是完全正确的。 显然，一个程序是完全正确的等价于该程序是部分正确的同时又是终止的。,10,程序正确性证明方法,FLOYD的不变式断言法（证明部分正确性） FLOYD良序集方法（证明终止性） Hoare的公理化方法（证明部分正确性）及其推广

4、（证明完全正确性） Dijstra的弱谓词置换法（证明完全正确性）,11,7.9.2 Floyd不变式断言法,建立断言 一个程序除了需要建立输入/输出断言外，如程序中出现循环，还要建立相应于该循环的不变式断言，称之为循环不变式断言。所谓循环不变式断言，是在循环中选一个断点，在断点处建立一个适当的断言，使循环每次执行到断点时，断言都为真。 建立检验条件 所谓检验条件就是程序运行通过某通路时应满足的条件。 证明检验条件 证明上面给定的所有检验条件，如果每一条通路的检验条件都为真，则该程序是部分正确的。,12,例子,设x1，x2是正整数，求最大公约数Z=gcd（x1，x2），其流程图如下图所示。试证

5、明它的部分正确性。,13,建立断言,输入断言（x）：x10 x20 输出断言（x，z）：z=gcd（x1，x2） 在断点B建立不变式断言P（x，y）： x10 x20y10y20gcd（y1，y2）=gcd（x1，x2）,这里，约定所有变量均为整型，且x表示（x1，x2），y表示（y1，y2）。,14,建立检验条件,选择B为断点，则程序的执行通路为： Path1：AB Path2：BDB Path3：BEB Path4：BGC 对每条通路可建立相应的检验条件。,15,检验条件表示,设通路i的输入/输出断言分别为i（x,y）和i（x，y），而通过此通路的条件为Ri(x,y)，通过此通路后y的值变

6、为ri(x,y)，则应有检验条件： i（x，y）Ri（x，y）i（x，ri（x，y） 其中，y表示程序执行中的一组中间变量，x是输入量。符号表示蕴涵逻辑关系。,16,Path1检验条件,1（x，y）为（x）；R1（x，y）恒真，即无条件通过； 1（x，y）为P（x，y）；通过此通路后y的值取值x。 故有：（x）P（x，x），即 x10 x20 x10 x20 x10 x20gcd（x1，x2）=gcd（x1，x2）,其它路径的检验条件（略）,17,证明检验条件,对任意正整数y1和y2有如下关系： 1若y1y2则gcd(y1,y2)=gcd(y1-y2,y2)； 2若y2y1则gcd(y1,y2

7、)=gcd(y1,y2-y1)； 3若y1=y2则gcd(y1,y2)=y1=y2。,对于Path1，其检验条件显然是成立的；,其它（略）,18,7.9.3 Floyd良序集方法,如果一个非空集合W关于二元关系- a1 - a2 - 其中a0，a1，a2,.W。,19,证明步骤,设程序P的输入断言为（x），良序集法证明P关于（x）是终止的证明步骤 （1）选取一个点集合截断程序的各个循环部分，在每一个截断点i处建立一个中间断言qi（x，y）。 （2）选取一个良序集（W，- Ej（x，r（x，y） 显然，如果所有的终止条件成立，则程序P一定终止。,20,例子,对任一给定的自然数X，计算Z= （即Z

8、等于x的平方根取整）的程序流程图如图所示。,21,截断程序的循环部分,该程序只有一个循环，在B点将循环断开，并建立断点断言： q（x，y）：y30 y2x,22,选取良序集,选取良序集为（N，），N为自然数集合。定义B点的终止表达式为： E（x，y）：x-y2,23,证明所选取的断言是“良断言”,1对通路AB（从程序入口点A到截断点B）有： （x）RAB（x，y）q（x，rAB（x，y） 显然RAB（x，y）恒为真，即走AB的条件恒真； rAB（x，y）为（0，0，1），即y的值通过AB后变为(0,0,1)。y表示（y1,y2,y3）。 故有（x）q（x，0，0，1） 即 x010 0 x 显

9、然,此蕴涵式成立；,其它（略）,24,证明终止表达式是良函数,即证明：q（x，y）E（x，y）N 即y30y2xx-y20 x-y2N 此蕴涵式显然也成立。,25,证明终止条件成立,即对于断点B到断B的通路（BCDB）有： q（x，y）RBCDB（x，y）E（x，y）E（x，rBCDB（x，y） 即：y30y2xy2+y3xx-y2x-(y2+y3) 由蕴涵式的前项有: y2x且y2+y3x故 x-y20 即x-y2N x-(y2+y3)0 即x-(y2+y3)N 同时y30，故有x-y2X-（y2+y3）且均属于集合（N，）中。 至此，也就证明了该程序的终止性。,26,7.9.4 程序正确性

10、证明的局限性,经验表明，程序证明实现的困难在于寻找程序的循环结构所蕴涵的循环不变式。 只有当程序“做什么”的说明能以简单的函数给出时，才能使用程序正确性证明技术。而大型问题就难以给出这种说明。因此，在实际应用中还存在一些问题。 所依赖的数学基础太强，用起来不够自然，数学素质不强的人很难接受。另外，证明本身也不能保证无错。,27,7.10 调 试,调试，又称纠错或排错，是程序测试后开始的工作，主要任务是依据测试发现的错误迹象确定错误位置和原因，并加以改正。 调试活动由两部分组成： 确定程序中可疑错误的确切性质和位置。 对程序（设计，编码）进行修改，排除这个错误。 调试是通过现象，找出原因的一个思

11、维分析的过程。,28,7.10.1 调试的步骤,从错误的外部表现形式入手，确定程序中出错位置； 研究有关部分的程序，找出错误的内在原因； 修改设计和代码，以排除这个错误； 重复进行暴露了这个错误的原始测试或某些有关测试，以确认该错误是否被排除；是否引进了新的错误。 如果所做的修正无效，则撤消这次改动，重复上述过程，直到找到一个有效的解决办法为止。,29,调试难点,错误的症状和引起错误的原因可能相隔很远，尤其是在高度耦合的程序结构中； 错误症状可能在另一错误被纠正后消失或暂时性的消失； 错误症状可能实际并不是由错误引起的（如舍入误差）； 错误症状可能是由不易跟踪的人工操作引起的； 错误症状可能是

12、和时间相关的，而不是处理问题； 很难再现产生错误症状的输入条件； 错误症状可能时有时无（如在软硬件结合的嵌入式系统中常常遇到）； 错误症状可能是由于把任务分布在若干不同处理器上运行而造成。,30,7.10.2 调试的策略之一：猜测法,该方法通过分析错误症状，根据以往经验，辅助使用已有的计算机工具，猜测错误的原因并进行定位。可以通过“在程序中插入打印语句”、“使用注释或GOTO语句运行部分程序”或“调试工具”等来实现该方法。,31,跟踪法,先分析错误征兆，确定最先发现“症状”的位置。然后，人工沿程序的控制流程，向回追踪源程序代码，直到找到错误根源或确定错误产生的范围。 跟踪法对于小程序很有效，往往能把错误范围缩小到程序中的一小段代码；仔细分析这段代码不难确定出错的准确位置。但对于大程序，由于回溯的路径数目较多，回溯会变得很困难。,32,演绎法,演绎法排错是测试人员首先根据已有的测试用例，设想及枚举出所有可能出错的原因做为假设；然后再用原始测试数据或新的测试，从中逐个排除不可能正确的假设；最后，再用测试数据验证余下的假设确是出错的原因。,33,归纳法,归纳法排错的基本思想是：从一些线索（错误征兆）着手，通过分析它们之间的关系来找出错误。,34,7.10