软件验证技术PPT课件

1、中南大学 信息科学与工程学院 任胜兵主要内容 程序正确性证明 调试第1页/共34页中南大学 信息科学与工程学院 任胜兵7.9 程序正确性证明 测试可以帮助人们发现程序中的错误，但它却不能证明程序中没有错误。 早在50年代，图林（Turing）等人就开始注意并开展了程序正确性证明这方面的早期研究工作；60年代后半期，Floyd和Hoare等人提出了不变式断言法和公理化方法，使得这一研究进入了一个蓬勃发展的新阶段；在此之后，出现了许多不同的程序正确性证明方法。 第2页/共34页中南大学 信息科学与工程学院 任胜兵7.9.1 程序正确性定义 所谓一段程序是正确的，是指这段程序能准确无误地完成预定的功

2、能。或者说，对任何一组允许的输入，程序执行后能得到一组相应的正确的输出。 在研究程序正确性证明时，将一段程序的输入和输出应满足的条件的逻辑关系式分别称为此段程序的输入断言（或初始断言、前置断言）和输出断言（或结果断言、后置断言），通常用谓词(x)和(x，z)表示，其中x和z分别表示输入和输出数据（可以是一个或一组变量）。第3页/共34页中南大学 信息科学与工程学院 任胜兵例子 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,

3、y,z):z=yx。 第4页/共34页中南大学 信息科学与工程学院 任胜兵程序正确性三种类型 程序的部分正确性 程序的终止性 程序的完全正确性 第5页/共34页中南大学 信息科学与工程学院 任胜兵程序的部分正确性 若每一个使得（x）为真且程序计算终止的输入数据x，（x，p（x）都为真，则称程序p关于和是部分正确的。 这里p（x）表示与输入数据x相对应的程序p的输出数据。第6页/共34页中南大学 信息科学与工程学院 任胜兵程序的终止性 若每一个使得（x）为真的输入数据x，程序计算都终止，则称程序P对是终止的。 第7页/共34页中南大学 信息科学与工程学院 任胜兵程序的完全正确性 若每一个使得（x

4、）为真的输入数据x，程序计算都终止且（x，P（x）为真，则称程序P关于和是完全正确的。 显然，一个程序是完全正确的等价于该程序是部分正确的同时又是终止的。 第8页/共34页中南大学 信息科学与工程学院 任胜兵程序正确性证明方法 FLOYD的不变式断言法（证明部分正确性） FLOYD良序集方法（证明终止性） Hoare的公理化方法（证明部分正确性）及其推广（证明完全正确性） Dijstra的弱谓词置换法（证明完全正确性） 第9页/共34页中南大学 信息科学与工程学院 任胜兵7.9.2 Floyd不变式断言法 建立断言 一个程序除了需要建立输入/输出断言外，如程序中出现循环，还要建立相应于该循环的

5、不变式断言，称之为循环不变式断言。所谓循环不变式断言，是在循环中选一个断点，在断点处建立一个适当的断言，使循环每次执行到断点时，断言都为真。 建立检验条件 所谓检验条件就是程序运行通过某通路时应满足的条件。 证明检验条件 证明上面给定的所有检验条件，如果每一条通路的检验条件都为真，则该程序是部分正确的。第10页/共34页中南大学 信息科学与工程学院 任胜兵例子 设x1，x2是正整数，求最大公约数Z=gcd（x1，x2），其流程图如下图所示。试证明它的部分正确性。 第11页/共34页中南大学 信息科学与工程学院 任胜兵建立断言 输入断言（x）：x10 x20 输出断言（x，z）：z=gcd（x1

6、，x2） 在断点B建立不变式断言P（x，y）： x10 x20y10y20gcd（y1，y2）=gcd（x1，x2）这里，约定所有变量均为整型，且x表示（x1，x2），y表示（y1，y2）。第12页/共34页中南大学 信息科学与工程学院 任胜兵建立检验条件 选择B为断点，则程序的执行通路为：Path1：ABPath2：BDBPath3：BEBPath4：BGC 对每条通路可建立相应的检验条件。第13页/共34页中南大学 信息科学与工程学院 任胜兵检验条件表示设通路i的输入/输出断言分别为i（x,y）和i（x，y），而通过此通路的条件为Ri(x,y)，通过此通路后y的值变为ri(x,y)，则应有

7、检验条件： i（x，y）Ri（x，y）i（x，ri（x，y） 其中，y表示程序执行中的一组中间变量，x是输入量。符号表示蕴涵逻辑关系。第14页/共34页中南大学 信息科学与工程学院 任胜兵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）其它路径的检验条件（略）第15页/共34页中南大学 信息科学与工程学院 任胜兵证明检验条件 对任意正整数y1和y2有如下关系： 1若y1y2则gcd(y1,y2

8、)=gcd(y1-y2,y2)； 2若y2y1则gcd(y1,y2)=gcd(y1,y2-y1)； 3若y1=y2则gcd(y1,y2)=y1=y2。 对于Path1，其检验条件显然是成立的； 其它（略）第16页/共34页中南大学 信息科学与工程学院 任胜兵7.9.3 Floyd良序集方法 如果一个非空集合W关于二元关系-是良序的，则集合W应满足：W为具有关系-的偏序集。 即关系-满足下列性质： 1传递性，即对一切a，b，cW，如果a-b，b-c则有a-c。 2反对称性，即对一切a，bW，如果a-b，则有b-a。 3反自反性，即对一切aW，a - a1 - a2 - 其中a0，a1，a2,.W

9、。 第17页/共34页中南大学 信息科学与工程学院 任胜兵证明步骤 设程序P的输入断言为（x），良序集法证明P关于（x）是终止的证明步骤 （1）选取一个点集合截断程序的各个循环部分，在每一个截断点i处建立一个中间断言qi（x，y）。 （2）选取一个良序集（W，- Ej（x，r（x，y）显然，如果所有的终止条件成立，则程序P一定终止。第18页/共34页中南大学 信息科学与工程学院 任胜兵例子 对任一给定的自然数X，计算Z= （即Z等于x的平方根取整）的程序流程图如图所示。 X第19页/共34页中南大学 信息科学与工程学院 任胜兵截断程序的循环部分 该程序只有一个循环，在B点将循环断开，并建立断点

10、断言：q（x，y）：y30 y2x第20页/共34页中南大学 信息科学与工程学院 任胜兵选取良序集 选取良序集为（N，0，故有x-y2X-（y2+y3）且均属于集合（N，）中。至此，也就证明了该程序的终止性。第24页/共34页中南大学 信息科学与工程学院 任胜兵7.9.4 程序正确性证明的局限性 经验表明，程序证明实现的困难在于寻找程序的循环结构所蕴涵的循环不变式。 只有当程序“做什么”的说明能以简单的函数给出时，才能使用程序正确性证明技术。而大型问题就难以给出这种说明。因此，在实际应用中还存在一些问题。 所依赖的数学基础太强，用起来不够自然，数学素质不强的人很难接受。另外，证明本身也不能保证

11、无错。第25页/共34页中南大学 信息科学与工程学院 任胜兵7.10 调 试 q调试，又称纠错或排错，是程序测试后开始的工作，主要任务是依据测试发现的错误迹象确定错误位置和原因，并加以改正。q调试活动由两部分组成： 确定程序中可疑错误的确切性质和位置。 对程序（设计，编码）进行修改，排除这个错误。q调试是通过现象，找出原因的一个思维分析的过程。第26页/共34页中南大学 信息科学与工程学院 任胜兵7.10.1 调试的步骤 n从错误的外部表现形式入手，确定程序中出错位置；n研究有关部分的程序，找出错误的内在原因；n修改设计和代码，以排除这个错误；n重复进行暴露了这个错误的原始测试或某些有关测试，

12、以确认该错误是否被排除；是否引进了新的错误。n如果所做的修正无效，则撤消这次改动，重复上述过程，直到找到一个有效的解决办法为止。第27页/共34页中南大学 信息科学与工程学院 任胜兵调试难点 错误的症状和引起错误的原因可能相隔很远，尤其是在高度耦合的程序结构中； 错误症状可能在另一错误被纠正后消失或暂时性的消失； 错误症状可能实际并不是由错误引起的（如舍入误差）； 错误症状可能是由不易跟踪的人工操作引起的； 错误症状可能是和时间相关的，而不是处理问题； 很难再现产生错误症状的输入条件； 错误症状可能时有时无（如在软硬件结合的嵌入式系统中常常遇到）； 错误症状可能是由于把任务分布在若干不同处理器

13、上运行而造成。 第28页/共34页中南大学 信息科学与工程学院 任胜兵7.10.2 调试的策略之一：猜测法 该方法通过分析错误症状，根据以往经验，辅助使用已有的计算机工具，猜测错误的原因并进行定位。可以通过“在程序中插入打印语句”、“使用注释或GOTO语句运行部分程序”或“调试工具”等来实现该方法。第29页/共34页中南大学 信息科学与工程学院 任胜兵跟踪法 n先分析错误征兆，确定最先发现“症状”的位置。然后，人工沿程序的控制流程，向回追踪源程序代码，直到找到错误根源或确定错误产生的范围。n跟踪法对于小程序很有效，往往能把错误范围缩小到程序中的一小段代码；仔细分析这段代码不难确定出错的准确位置

14、。但对于大程序，由于回溯的路径数目较多，回溯会变得很困难。第30页/共34页中南大学 信息科学与工程学院 任胜兵演绎法无剩余列举可能的原因排除不会发生的原因细析余下的原因证明假设纠正错误收集更多的测试结果有剩余不能能 演绎法排错是测试人员首先根据已有的测试用例，设想及枚举出所有可能出错的原因做为假设；然后再用原始测试数据或新的测试，从中逐个排除不可能正确的假设；最后，再用测试数据验证余下的假设确是出错的原因。第31页/共34页中南大学 信息科学与工程学院 任胜兵归纳法 归纳法排错的基本思想是：从一些线索（错误征兆）着手，通过分析它们之间的关系来找出错误。收集有关数据组织数据研究数据间的关系提出假设证明假设纠正错误能不能能不能第32页/共34页中南大学 信息科学与工程学院 任胜兵7.10.3 调试的原则 综合起来