第7章 软件验证技术
(第7.9-7.10节）
中南大学 信息科学与工程学院 任胜兵
主要内容
程序正确性证明 调试
中南大学 信息科学与工程学院 任胜兵
7.9 程序正确性证明
测试可以帮助人们发现程序中的错误，但它却 不能证明程序中没有错误。 早在50年代，图林（Turing）等人就开始注意 并开展了程序正确性证明这方面的早期研究工 作；60年代后半期，Floyd和Hoare等人提出了 不变式断言法和公理化方法，使得这一研究进 入了一个蓬勃发展的新阶段；在此之后，出现 了许多不同的程序正确性证明方法。
中南大学 信息科学与工程学院 任胜兵
7.10.2 调试的策略之一：猜测法
该方法通过分析错误症状，根据以往 经验，辅助使用已有的计算机工具，猜 测错误的原因并进行定位。可以通过 “在程序中插入打印语句”、“使用注 释或GOTO语句运行部分程序”或“调试 工具”等来实现该方法。
中南大学 信息科学与工程学院 任胜兵
中南大学 信息科学与工程学院 任胜兵
调试难点
错误的症状和引起错误的原因可能相隔很远，尤其是在高度 耦合的程序结构中； 错误症状可能在另一错误被纠正后消失或暂时性的消失； 错误症状可能实际并不是由错误引起的（如舍入误差）； 错误症状可能是由不易跟踪的人工操作引起的； 错误症状可能是和时间相关的，而不是处理问题； 很难再现产生错误症状的输入条件； 错误症状可能时有时无（如在软硬件结合的嵌入式系统中常 常遇到）； 错误症状可能是由于把任务分布在若干不同处理器上运行而 造成。
证明上面给定的所有检验条件，如果每一条通路的检验条件 都为真，则该程序是部分正确的。
中南大学 信息科学与工程学院 任胜兵
例子
设x1，x2是正整数，求最大公约数Z=gcd（x1，x2），其 流程图如下图所示。试证明它的部分正确性。
中南大学 信息科学与工程学院 任胜兵
建立断言
输入断言φ（x）：x1＞0 ∧ x2＞0 输出断言ψ（x，z）：z=gcd（x1，x2） 在断点B建立不变式断言P（x，y）：
中南大学 信息科学与工程学院 任胜兵
证明步骤
设程序P的输入断言为φ （x），良序集法证明P关于φ （x）是终止的证明步骤 （1）选取一个点集合截断程序的各个循环部分，在每一个截断点i处建立一个中间断言qi（x，y）。 （2）选取一个良序集（W，-< ），在每一个截断点i处定义一个终止表达式E i（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，且是某个循环的一部分的通路α有： ∧Rα（x，y）[Ei（x，y）>- Ej（x，rα（x，y））] 显然，如果所有的终止条件成立，则程序P一定终止。 q i （x ， y ）
[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，其检验条件显然是成立的； 其它（略）
跟踪法


先分析错误征兆，确定最先发现“症状” 的位置。然后，人工沿程序的控制流程， 向回追踪源程序代码，直到找到错误根源 或确定错误产生的范围。 跟踪法对于小程序很有效，往往能把错误 范围缩小到程序中的一小段代码；仔细分 析这段代码不难确定出错的准确位置。但 对于大程序，由于回溯的路径数目较多， 回溯会变得很困难。
中南大学 信息科学与工程学院 任胜兵
程序的终止性
若每一个使得φ（x）为真的输入数据x， 程序计算都终止，则称程序P对φ是终止 的。
中南大学 信息科学与工程学院 任胜兵
程序的完全正确性
若每一个使得φ（x）为真的输入数据x， 程序计算都终止且 ψ （x，P（ x））为真， 则称程序P关于φ和ψ是完全正确的。 显然，一个程序是完全正确的等价于该 程序是部分正确的同时又是终止的。

中南大学 信息科学与工程学院 任胜兵
7.10.1 调试的步骤


从错误的外部表现形式入手，确定程序中出错位置； 研究有关部分的程序，找出错误的内在原因； 修改设计和代码，以排除这个错误； 重复进行暴露了这个错误的原始测试或某些有关测 试，以确认该错误是否被排除；是否引进了新的错 误。 如果所做的修正无效，则撤消这次改动，重复上述 过程，直到找到一个有效的解决办法为止。
其中， y 表示程序执行中的一组中间变 量，x是输入量。符号表示蕴涵逻辑关 系。
中南大学 信息科学与工程学院 任胜兵
Path1检验条件
φ 1 （ x ， y ）为 φ （ x ）； R 1 （ x ， y ）恒真，即无 条件通过； ψ1（x，y）为P（x，y）；通过此通路后y的值取 值x。 故有：φ（x）P（x，x），即
中南大学 信息科学与工程学院 任胜兵
例子
对任一给定的自然数X，计算Z=[ X ] （即Z等于x的平方根取整）的程序流程 图如图所示。
中南大学 信息科学与工程学院 任胜兵
截断程序的循环部分
该程序只有一个循环，在B点将循环断开， 并建立断点断言： q（x，y）：y3＞0 ∧ y2≤x
中南大学 信息科学与工程学院 任胜兵
中南大学 信息科学与工程学院 任胜兵
7.9.1 程序正确性定义
所谓一段程序是正确的，是指这段程序能准确 无误地完成预定的功能。或者说，对任何一组 允许的输入，程序执行后能得到一组相应的正 确的输出。 在研究程序正确性证明时，将一段程序的输入 和输出应满足的条件的逻辑关系式分别称为此 段程序的输入断言（或初始断言、前置断言） 和输出断言（或结果断言、后置断言），通常 用谓词φ(x)和ψ(x，z)表示，其中x和z分别表示 输入和输出数据（可以是一个或一组变量）。
x1＞0∧x2＞0∧y1＞0∧y2＞0∧gcd（y1，y2）=gcd（x1，x2）
这里，约定所有变量均为 整型，且 x 表示（ x 1 ， x 2 ）， y表示（y1，y2）。
中南大学 信息科学与工程学院 任胜兵
建立检验条件
选择B为断点，则程序的执行通路为： Path1：A→B Path2：B→D→B Path3：B→E→B Path4：B→G→C 对每条通路可建立相应的检验条件。
中南大学 信息科学与工程学院 任胜兵
演绎法
演绎法排错是测试人员首先根据已有的测 试用例，设想及枚举出所有可能出错的原因做为 假设；然后再用原始测试数据或新的测试，从中 逐个排除不可能正确的假设；最后，再用测试数 据验证余下的假设确是出错的原因。
建立断言
一个程序除了需要建立输入 /输出断言外，如程序中出现循环， 还要建立相应于该循环的不变式断言，称之为循环不变式断言。 所谓循环不变式断言，是在循环中选一个断点，在断点处建立一 个适当的断言，使循环每次执行到断点时，断言都为真。
建立检验条件
所谓检验条件就是程序运行通过某通路时应满足的条件。
证明检验条件
选取良序集
选取良序集为（ 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的条件恒真；
中南大学 信息科学与工程学院 任胜兵
7.9.4 程序正确性证明的局限性
经验表明，程序证明实现的困难在于寻找程序 的循环结构所蕴涵的循环不变式。 只有当程序“做什么”的说明能以简单的函数 给出时，才能使用程序正确性证明技术。而大 型问题就难以给出这种说明。因此，在实际应 用中还存在一些问题。 所依赖的数学基础太强，用起来不够自然，数 学素质不强的人很难接受。另外，证明本身也 不能保证无错。
中南大学 信息科学与工程学院 任胜兵
检验条件ቤተ መጻሕፍቲ ባይዱ示
设通路 i 的输入 / 输出断言分别为 φ i （ x,y ） 和 ψ i （ x ， y ），而通过此通路的条件为 R i (x,y) ，通过此通路后 y 的值变为 r i (x,y) ， 则应有检验条件：
φi（x，y）∧Ri（x，y）ψi（x，ri（x，y））
中南大学 信息科学与工程学院 任胜兵
例子
unsigned power(unsigned x,unsigned y)
{ unsigned z;
z=1; while (x!=0) { z=z*y; x=x-1; } return z; } 则 φ(x,y):x≥0, y＞0；
ψ(x,y,z):z=yx。 中南大学 信息科学与工程学院 任胜兵
即[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∈N x-(y2+y3)≥0 即x-(y2+y3)∈N 同时y3>0，故有x-y2〉X-（y2+y3）且均属于集合（N，〈）中。 至此，也就证明了该程序的终止性。