第5章软件验证技术(5.9-5.10)

第5章软件验证技术

(第5.9-5.10节）武汉纺织大学数学与计算机学院主要内容程序正确性证明调试武汉纺织大学数学与计算机学院5.9程序正确性证明

测试可以帮助人们发现程序中的错误，但它却不能证明程序中没有错误。早在50年代，图林（Turing）等人就开始注意并开展了程序正确性证明这方面的早期研究工作；60年代后半期，Floyd和Hoare等人提出了不变式断言法和公理化方法，使得这一研究进入了一个蓬勃发展的新阶段；在此之后，出现了许多不同的程序正确性证明方法。武汉纺织大学数学与计算机学院5.9.1程序正确性定义

所谓一段程序是正确的，是指这段程序能准确无误地完成预定的功能。或者说，对任何一组允许的输入，程序执行后能得到一组相应的正确的输出。在研究程序正确性证明时，将一段程序的输入和输出应满足的条件的逻辑关系式分别称为此段程序的输入断言（或初始断言、前置断言）和输出断言（或结果断言、后置断言），通常用谓词φ(x)和ψ(x，z)表示，其中x和z分别表示输入和输出数据（可以是一个或一组变量）。武汉纺织大学数学与计算机学院例子unsignedpower(unsignedx,unsignedy){unsignedz;z=1;while(x!=0){z=z*y;x=x-1;}returnz;}则φ(x,y):x≥0,y＞0；ψ(x,y,z):z=yx。武汉纺织大学数学与计算机学院程序正确性三种类型程序的部分正确性程序的终止性程序的完全正确性武汉纺织大学数学与计算机学院程序的部分正确性若每一个使得φ（x）为真且程序计算终止的输入数据x，ψ（x，p（x））都为真，则称程序p关于φ和ψ是部分正确的。这里p（x）表示与输入数据x相对应的程序p的输出数据。武汉纺织大学数学与计算机学院程序的终止性若每一个使得φ（x）为真的输入数据x，程序计算都终止，则称程序P对φ是终止的。武汉纺织大学数学与计算机学院程序的完全正确性若每一个使得φ（x）为真的输入数据x，程序计算都终止且ψ（x，P（x））为真，则称程序P关于φ和ψ是完全正确的。显然，一个程序是完全正确的等价于该程序是部分正确的同时又是终止的。转到武汉纺织大学数学与计算机学院程序正确性证明方法FLOYD的不变式断言法（证明部分正确性）FLOYD良序集方法（证明终止性）Hoare的公理化方法（证明部分正确性）及其推广（证明完全正确性）Dijstra的弱谓词置换法（证明完全正确性）武汉纺织大学数学与计算机学院5.9.2Floyd不变式断言法

建立断言

一个程序除了需要建立输入/输出断言外，如程序中出现循环，还要建立相应于该循环的不变式断言，称之为循环不变式断言。所谓循环不变式断言，是在循环中选一个断点，在断点处建立一个适当的断言，使循环每次执行到断点时，断言都为真。建立检验条件

所谓检验条件就是程序运行通过某通路时应满足的条件。证明检验条件

证明上面给定的所有检验条件，如果每一条通路的检验条件都为真，则该程序是部分正确的。武汉纺织大学数学与计算机学院例子设x1，x2是正整数，求最大公约数Z=gcd（x1，x2），其流程图如下图所示。试证明它的部分正确性。

武汉纺织大学数学与计算机学院建立断言

输入断言φ（x）：x1＞0∧x2＞0输出断言ψ（x，z）：z=gcd（x1，x2）在断点B建立不变式断言P（x，y）：

x1＞0∧x2＞0∧y1＞0∧y2＞0∧gcd（y1，y2）=gcd（x1，x2）这里，约定所有变量均为整型，且x表示（x1，x2），y表示（y1，y2）。武汉纺织大学数学与计算机学院建立检验条件

选择B为断点，则程序的执行通路为：Path1：A→BPath2：B→D→BPath3：B→E→BPath4：B→G→C对每条通路可建立相应的检验条件。武汉纺织大学数学与计算机学院检验条件表示设通路i的输入/输出断言分别为φi（x,y）和ψi（x，y），而通过此通路的条件为Ri(x,y)，通过此通路后y的值变为ri(x,y)，则应有检验条件：φi（x，y）∧Ri（x，y）ψi（x，ri（x，y））其中，y表示程序执行中的一组中间变量，x是输入量。符号表示蕴涵逻辑关系。武汉纺织大学数学与计算机学院Path1检验条件φ1（x，y）为φ（x）；R1（x，y）恒真，即无条件通过；ψ1（x，y）为P（x，y）；通过此通路后y的值取值x。故有：φ（x）P（x，x），即[x1＞0∧x2＞0][x1＞0∧x2＞0∧x1＞0∧x2＞0∧gcd（x1，x2）=gcd（x1，x2）]其它路径的检验条件（略）武汉纺织大学数学与计算机学院证明检验条件

对任意正整数y1和y2有如下关系：1°若y1>y2则gcd(y1,y2)=gcd(y1-y2,y2)；2°若y2>y1则gcd(y1,y2)=gcd(y1,y2-y1)；3°若y1=y2则gcd(y1,y2)=y1=y2。

对于Path1，其检验条件显然是成立的；

其它（略）武汉纺织大学数学与计算机学院5.9.3Floyd良序集方法

如果一个非空集合W关于二元关系-<是良序的，则集合W应满足：①W为具有关系-<的偏序集。即关系-<满足下列性质：1°传递性，即对一切a，b，c∈W，如果a-<b，b-<c则有a-<c。2°反对称性，即对一切a，b∈W，如果a-<b，则有b-<a。3°反自反性，即对一切a∈W，a-<a。②W的每一非空子集都有一个“最小”元素。即不存在由W中的元素构成的无限递减序列：a0>-a1>-a2>-……其中a0，a1，a2,...∈W。武汉纺织大学数学与计算机学院证明步骤

设程序P的输入断言为φ（x），良序集法证明P关于φ（x）是终止的证明步骤

（1）选取一个点集合截断程序的各个循环部分，在每一个截断点i处建立一个中间断言qi（x，y）。（2）选取一个良序集（W，-<），在每一个截断点i处定义一个终止表达式Ei（x，y）。（3）证明所选取的断言是“良断言”。即对每一个从程序入口到断点j的通路α有：φ（x）∧Rα（x，y）qj（x，rα（x，y））成立；而对每一个由断点i到断点j的通路α有：qi（x，y）∧Rα（x，y）qj（x，rα（x，y））成立。这里Rα和rα分别表示通过通路α的条件及通过通路α以后变量y的值。另外，在这两个蕴涵式中省略了全称量词xy，以下两步亦如此。（4）证明终止表达式是“良函数”。即对每个断点i有：qi（x，y）Ei（x，y）∈W（5）证明终止条件成立。即对于每一条从断点i到断点j，且是某个循环的一部分的通路α有：qi（x，y）∧Rα（x，y）[Ei（x，y）>-Ej（x，rα（x，y））]显然，如果所有的终止条件成立，则程序P一定终止。武汉纺织大学数学与计算机学院例子对任一给定的自然数X，计算Z=[]（即Z等于x的平方根取整）的程序流程图如图所示。

武汉纺织大学数学与计算机学院截断程序的循环部分

该程序只有一个循环，在B点将循环断开，并建立断点断言：q（x，y）：y3＞0∧y2≤x武汉纺织大学数学与计算机学院选取良序集

选取良序集为（N，<），N为自然数集合。定义B点的终止表达式为：E（x，y）：x-y2武汉纺织大学数学与计算机学院证明所选取的断言是“良断言”

1°对通路A→B（从程序入口点A到截断点B）有：φ（x）∧RA→B（x，y）q（x，rA→B（x，y））显然RA→B（x，y）恒为真，即走A→B的条件恒真；rA→B（x，y）为（0，0，1），即y的值通过A→B后变为(0,0,1)。y表示（y1,y2,y3）。故有φ（x）q（x，0，0，1）即x≥0[1＞0∧0≤x]显然,此蕴涵式成立；其它（略）武汉纺织大学数学与计算机学院证明终止表达式是良函数

即证明：q（x，y）E（x，y）∈N即[y3＞0∧y2≤x]x-y2≥0x-y2∈N此蕴涵式显然也成立。武汉纺织大学数学与计算机学院证明终止条件成立

即对于断点B到断B的通路（B→C→D→B）有：q（x，y）∧RB→C→D→B（x，y）[E（x，y）＞E（x，rB→C→D→B（x，y））]即：[y3＞0∧y2≤x∧y2+y3≤x][x-y2＞x-(y2+y3)]由蕴涵式的前项有:y2≤x且y2+y3≤x故x-y2≥0即x-y2∈Nx-(y2+y3)≥0即x-(y2+y3)∈N同时y3>0，故有x-y2〉X-（y2+y3）且均属于集合（N，〈）中。至此，也就证明了该程序的终止性。武汉纺织大学数学与计算机学院5.9.4程序正确性证明的局限性

经验表明，程序证明实现的困难在于寻找程序的循环结构所蕴涵的循环不变式。只有当程序“做什么”的说明能以简单的函数给出时，才能使用程序正确性证明技术。而大型问题就难以给出这种说明。因此，在实际应用中还存在一些问题。所依赖的数学基础太强，用起来不够自然，数学素质不强的人很难接受。另外，证明本身也不能保证无错。武汉纺织大学数学与计算机学院补充：集成测试文档集成测试文档即测试说明书（testspecifications）应给出集成的总体规划和某些特殊测试的描述。它将作为软件配置的一部分提交给用户。测试说明书的主要内容提纲如下：武汉纺织大学数学与计算机学院测试说明书的主要内容提纲1）测试范围2）测试计划A．测试的各个阶段和划分模块群情况B．进度安排C．开销软件（驱动和桩模块）D．环境和资源武汉纺织大学数学与计算机学院3）各个模块群测试过程的描述，包括：A．集成的顺序①用途②被测模式B．模块群中各模块单元测试的情况①模块的测试描述②开销软件描述③期望的结果武汉纺织大学数学与计算机学院C．测试环境①特殊工具和技术②开销软件的描述D．测试用例E．模块群的期望结果等4）实际测试结果5）参考文献6）附录。武汉纺织大学数学与计算机学院5.10调

试

调试，又称纠错或排错，是程序测试后开始的工作，主要任务是依据测试发现的错误迹象确定错误位置和原因，并加以改正。调试活动由两部分组成：①确定程序中可疑错误的确切性质和位置。②对程序（设计，编码）进行修改，排除这个错误。调试是通过现象，找出原因的一个思维分析的过程。武汉纺织大学数学与计算机学院执行测试用例测试用例结果评估附加测试被怀疑的原因已识别的原因纠正回归测试测试过程武汉纺织大学数学与计算机学院5.10.1调试的步骤

从错误的外部表现形式入手，确定程序中出错位置；研究有关部分的程序，找出错误的内在原因；修改设计和代码，以排除这个错误；重复进行暴露了这个错误的原始测试或某些有关测试，以确认该错误是否被排除；是否引进了新的错误。如果所做的修正无效，则撤消这次改动，重复上述过程，直到找到一个有效的解决办法为止。武汉纺织大学数学与计算机学院调试难点错误的症状和引起错误的原因可能相隔很远，尤其是在高度耦合的程序结构中；错误症状可能在另一错误被纠正后消失或暂时性的消失；错误症状可能实际并不是由错误引起的（如舍入误差）；错误症状可能是由不易跟踪的人工操作引起的；错误症状可能是和时间相关的，而不是处理问题；很难再现产生错误症状的输入条件；错误症状可能时有时无（如在软硬件结合的嵌入式系统中常常遇到）；错误症状可能是由于把任务分布在若干不同处理器上运行而造成。

武汉纺织大学数学与计算机学院5.10.2调试的策略之一：猜测法

该方法通过分析错误症状，根据以往经验，辅助使用已有的计算机工具，猜测错误的原因并进行定位。可以通过“在程序中插入打印语句”、“使用注释或GOTO语句运行部分程序”或“调试工具”等来实现该方法。武汉纺织大学数学与计算机学院跟踪法

先分析错误征兆，确定最先发现“症状”的位置。然后，人工沿程序的控制流程，向回追踪源程序代码，直到找到错误根源或确定错误产生的范围。跟踪法对于小程序很有效，往往能把错误范围缩小到程序中的一小段代码；仔细分析这段代码不难确定出错的准确位置。但对于大程序，由于回溯的路径数目较多，回溯会变得很困难。武汉纺织大学数学与计算机学院演绎法演绎法排错是测试人员首先根据已有的测试用例，设想及枚举出所有可能出错的原因做为假设；然后再用原始测试数据或新的测试，从中逐个排除不可能正确的假设；最后，再用测试数据验证余下的假设确是出错的原因。武汉纺织大学数学与计算机学院列举可能的原因排除不正确的假设精化余下的假设证明假设收集更多数据纠正错误有剩余能不能无剩余演绎法：普通特殊从假设中逐步排除、精化，从而导出错误根源。武汉纺织大学数学与计算机学院列举所有可能出错原因的假设：把所有可能的错误原因列成表。进而可以组织、分析现有数据。利用已有的测试数据，排除不正确的假设：仔细分析已有的数据，寻找矛盾，力求排除前一步列出所有原因。如果所有原因都被排除了，则需要补充一些数据(测试用例)，以建立新的假设。改进余下的假设：利用已知的线索，进一步改进余下的假设，使之更具体化，以便可以精确地确定出错位置。证明余下的假设武汉纺织大学数学与计算机学院归纳法归纳法排错的基本思想是：从一些线索（错误征兆）着手，通过分析它们之间的