第六课
程序正确性证明
本章主要研究内容
? 基本概念
? 程序测试的基本方法
? 部分正确性证明方法
? 终止性证明方法
基本概念－ 程序正确性的定义
? 一段程序是正确的，是指这段程序能正确无误地完成程
序设计时所期望的功能。或者说：对任何一组允许的输入信
息，程序执行后能得到一组和这组输入信息相对应的正确的
输出信息。程序的正确性是衡量一个程序是否优秀的最基本
条件。
? 一段程序是错误的，是指（ 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
? 试测试下面这一程序
? Procedure P(var A,B:REAL)
? Begin
? If(A > 1)and(B = 0) then X:=X/A;
? If(A=2)or(X>1)then X:=X+1;
? end
测试用例举例
? 在执行这个程序时，
有各种不同的路径，
如：
? a b d
? a b e d
? a c b d
? a c b e d
测试用例举例
? 我们可用白盒子方法设计测试用例，其任务是
尽可能多地执行各种语句，以及调试到各种路
径。
? 如选择 A = 2,B = 0,X = 3
? 则可执行路径
? a c b e d
? 此时能覆盖到全部 2个计算框，可发现一般的语句
的错误
? 我们通常把这种注重语句的复盖叫, 语句复盖,
测试用例举例
? 如选择
? A = 3,B = 0,X = 1
? A = 2,B = 1,X = 3
? 则可执行的路径为
? a c b d
? a b e d
? 从所走路径来看，上面这组数据要全面一些，它不仅通过
全部两个计算框，而且第一个判别框的两边都执行过一次。
? 我们通常把这种注重选择测试的复盖叫做, 判定复盖,
程序测试
? 从以上两个例子可以看出，测试通常是
不充分的，它只能发现某些错误的存在，
而不能证明错误的不存在。
? 所有，在真正设计测试用例的过程种常
常要考虑经济性，可行性。
? 测试的关键就是如何设计好高效，可行
的用例程序。
程序测试
? 如选择
? A=2,B=0,X=4
? A=1,B=1,X=1
? 则可执行的路径为
? a c b e d
? a b d
? 从这组数据来看，它注意了 4个条件
A>1,B=0,A=2和 X>1的复盖。我们称这种注重判
断的复盖为, 条件复盖,
程序测试
? 以上这些数据虽然均达到一些测试目的，且各有侧重，但是都是
不充分的。
? 如从条件出发，用组合的办法使各个条件都能执行到，则我们可
以写出以下 8种条件组合：
? 1)A>1,B=0
? 2)A>1,B<>0;(<>是不等号 )
? 3)A<=1,B=0
? 4)A<=1,B<>0
? 5)A=2,X>1
? 6)A=2,X<=1
? 7)A<>2,X>1
? 8)A<>2,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
? 它们都能使各种条件均能出现一次。虽然这个组合
方法比较方便，逻辑也很清楚，且对执行条件来说
还是比较全面的，但是仍然又未走遍的路径，如 a c
b d
程序测试
? 在测试时，还
要注意到计算
机执行多个条
件的特点，即
它必须把多个
条件分解为简
单判别才能执
行，如上述例
子可分解为右
图。
例子 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和 QuickTest Professional作为自动化测试工
具, 推荐 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)∧R i(x,y)－ >Ψi(x,ri(x,y))
? （ 3）证明检验条件，即证明（ 2）中所列出的所有检验条件，
如果每一条通路上的检验条件都为真，则该程序是部分正确
的。
部分正确性证明 － 不变式断言法实例
? 例 1：设 x1,x2是正整数，求它们的最大公约数，
? z=gcd(x1,x2)
? 基本算法：对于任意正整数 x1,x2,有：
? （ 1）若 x1>x2,gcd(x1,x2)=gcd(x1-x2,x2)
? （ 2）若 x2>x1,gcd(x1,x2)=gcd(x1,x2-x1)
? （ 3）若 x1=x2,gcd(x1,x2)=x1=x2
? 即反复执行（ 1）或（ 2），直到出现（ 3）中的情况
部分正确性证明 － 不变式断言法实例
(x1,x2)->(y1,y2)
y1=y2
开始
y1>y2
y1 ->z
结束
y2-y1->y2y1-y2->y1
B······ P(x,y)
A······ Φ(x)
T
G
C······ Ψ(x,z)
F
ED
F
T
部分正确性证明 － 不变式断言法实例
? 利用不变式断言法实例证明该流程框图的部分正确性,
? (1) 建立断言
? 输入断言 Φ(x):x1>0∧x2>0
? 输出断言 Ψ(x,z):z=gcd(x1,x2)
? 考虑到存在循环，将循环在 B点断开，建立 B点的不变式断言：
? P(x,y):x1>0∧x2>0∧y1>0∧y2>0∧gcd(y1,y2)=gcd(x1,x2)
? 其中,x,y分别表示 (x1,x2),(y1,y2)。
? (2) 建立检验条件
? 将 B设为断点后，程序执行中所有可能的通路分解为：
? 通路 1,A->B
? 通路 2,B->D->B
? 通路 3,B->E->B
? 通路 4,B->G->C
部分正确性证明 － 不变式断言法实例
? 利用不变式断言法实例证明该流程框图的部分正确性,
? (1) 建立断言
? 输入断言 Φ(x):x1>0∧x2>0
? 输出断言 Ψ(x,z):z=gcd(x1,x2)
? 考虑到存在循环，将循环在 B点断开，建立 B点的不变式断言：
? P(x,y):x1>0∧x2>0∧y1>0∧y2>0∧gcd(y1,y2)=gcd(x1,x2)
? 其中,x,y分别表示 (x1,x2),(y1,y2)。
? (2) 建立检验条件
? 通路 1的检验条件, 通路 1（ A->B） 是无条件的,
? 即 R1(x,y)=1（恒为真），同时 Φ1(x)－ > P(x,y),具体可写为：
? ［ x1>0∧x2>0] ->[x1>0∧x2>0∧y1>0∧y2>0∧gcd(y1,y2)=gcd(x1,x2)]
部分正确性证明 － 不变式断言法实例
? 通路 2的检验条件, R2(x,y)=[y1≠y2 ∧y1>y2>],通路 2的输入、输出
断言均为,P(x,y),因而检验条件为：
? ［ P(x,y)∧y1≠y2∧y1>y2>] ->P(x,y1-y2,y2),也即：
? [x1>0∧x2>0∧y1>0∧y2>0∧gcd(y1,y2)=gcd(x1,x2)
∧y1≠y2∧y1>y2] ->[x1>0∧x2>0∧(y1 -y2)>0∧y2>0∧gcd(y1 -
y2,y2)=gcd(x1,x2)]
? 通路 3的检验条件, R3(x,y)=[y1≠y2 ∧y1<y2>],通路 3的输入、输出
断言均为,P(x,y),因而检验条件为：
? ［ P(x,y)∧y1≠y2∧y1<y2>] ->P(x,y1,y2-y1),也即：
? [x1>0∧x2>0∧y1>0∧y2>0∧gcd(y1,y2)=gcd(x1,x2)
∧y1≠y2∧y1<y2] ->[x1>0∧x2>0∧y1>0∧(y2 -y1)>0∧gcd(y1,y2 -
y1)=gcd(x1,x2)]
? 通路 4的检验条件, R4(x,y)=[y1=y2],通路 4的输入断言为 P(x,y),
输出断言为 Ψ(x1,y2),检验条件为：
? ［ P(x,y)∧y1=y2] ->Ψ(x1,y2)
考试时间
?下周四晚 7,00------9,30
?地点西 12 S401到 S404,S406到
S412
?周五上课时间、地点不变
部分正确性证明 － 不变式断言法实例
? （ 3）证明检验条件是否成立
? 通路 1、通路 4的检验条件为真
? 对于 通路 2，检验条件为：
? [x1>0∧x2>0∧y1>0∧y2>0∧gcd(y1,y2)=gcd(x1,x2)
∧y1≠y2∧y1>y2] ->[x1>0∧x2>0∧(y1 -y2)>0∧y2>0∧gcd(y1 -
y2,y2)=gcd(x1,x2)]
? 检验条件的前项为真（成立）时,[y1>y2]->[y1-y2>0],更求最
大公约数的辗转算法,gcd(y1-y2,y2)=gcd(y1,y2)=gcd(x1,x2)，
此时,检验条件的后项为真（成立），因此，整个蕴涵运算为真，
即检验条件为真。
? 同理可证条件 3成立。
? 整个流程图的部分正确性得到了证明。
部分正确性证明 － 不变式断言法实例
不变式断言法也可以直接用于高级语言写出的程序。具体使用时，
以注释的形式在程序的断点处加上断言。
? 例 2：设 x,y是非负整数，求它们的最大公约数，
? z=gcd(x,y)
? Program A
? var x,y,z,s:integer;
? begin
? read(x,y);
? while x≠0 do
? if y>=x then y:=y-x
? else
? begin
? s:=x;x:=y;y:=s;
? end
? z:=y;
? write(z);
? end
部分正确性证明 － 不变式断言法实例
(1)建立断言 。 设 x,y的初始值为 x0,y0,
输入断言,Φ(x):x0>=0∧y0>=0∧(x0≠0∨y0≠0)
? 输出断言 Ψ(x,z):z=gcd(x0,y0)
? 不变式断言：
? P(x,y):x>=0∧y>=0∧(x0≠0∨y0≠0)∧gcd(x,y)=gcd(x0,y0)
? 将断言直接写入程序中：
? Program A
? var x,y,z,s:integer;
? begin
? read(x,y);
? ｛ x0>=0∧y0>=0∧(x0≠0∨y0≠0) ｝ //输入断言
? while x≠0 do
? L：｛ x>=0∧y>=0∧(x0≠0∨y0≠0)∧gcd(x,y)=gcd(x0,y0) ｝ //不变式断言
? if y>=x then y:=y-x
? else
? begin
? s:=x;x:=y;y:=s;
? end
? z:=y;
? {z=gcd(x0,y0)} //输出断言
? write(z);
? end
部分正确性证明 － 不变式断言法实例
(2)建立检验条件。设 x,y的初始值为 x0,y0,假定输入断言成立，即要证明
程序第一次执行到断点 L处时，不变式断言成立。此时的检验条件为：
检验条件 1：
［ x0>=0∧y0>=0∧(x0≠0∨y0≠0)] ->
[x0>=0∧y0>=0∧(x0≠0∨y0≠0)∧gcd(x,y)=gcd(x0,y0)]
进一步证明，当检验条件 1成立，程序控制循环后再次回到断点 L处时，不
变式断言仍然成立。程序控制循环再次回到断点 L处有两个途径，一个
是 y>=x成立时，另一个是 y<x时。当 y>=x成立时：
检验条件 2：
［ x>=0∧y>=0∧(x≠0∨y≠0)∧gcd(x,y)=gcd(x0,y0)∧x≠0∧y>=x] -
>[x>=0∧y -x>=0∧(x≠0∨y - x≠0)∧gcd(x,y - x)=gcd(x0,y0)]
当 y<x成立时：
检验条件 3：
［ x>=0∧y>=0∧(x≠0∨y≠0)∧gcd(x,y)=gcd(x0,y0)∧x≠0∧y<x] -
>[y>=0∧x>=0∧(y≠0∨x≠0)∧gcd(y,x)=gcd(x0,y0)]
部分正确性证明 － 不变式断言法实例
最后要证明如果不变时断言成立，但程序控制转出循环时，输出断言
成立。此时的检验条件为：
检验条件 4：
［ x>=0∧y>=0∧(x≠0∨y≠0)∧gcd(x,y)=gcd(x0,y0)∧x=0] -
>y=gcd(x0,y0)
(3)证明检验条件
条件 1：程序第一次执行到 L处时,x=x0,y=y0,gcd(x,y)=gcd(x0,y0)
成立，整个检验条件 1成立。
条件 2：如果蕴涵式前项成立，由 x>=0,y>=x成立可以推导出：
x>=0∧y -x>=0成立。由 x≠0 成立可以推导出,x≠0∨y - x≠0 成
立,再根据数论中辗转法可知,y>=x时,gcd(x,y)=gcd(x,y - x)
成立，而 gcd(x,y)=gcd(x0,y0)成立，因此 gcd(x,y -
x)=gcd(x0,y0)成立，由此，条件 2为真。
条件 3：如果蕴涵式前项成立，由 x,y互换，由合适公式的互换定律，
可以推导出条件 2为真。
部分正确性证明 － 不变式断言法实例
条件 4：如果蕴涵式前项成立，由
x>=0∧y>=0∧(x≠0∨y≠0)∧gcd(x,y)=gcd(x0,y0)∧x=0 可以推出
x=0,再由 (x≠0∨y≠0) 成立可以推导出 y>0 。再根据数论中辗转法
可知,x=0,y>0时,gcd(0,y)=y成立，由此，条件 4为真。
整个程序的部分正确性得以证明。
整个程序的部分正确性不能保证整个程序的完全正确性。
在例 1中，若将问题前提改为与例 2一致：设 x1,x2是非负整数，求它
们的最大公约数,z=gcd(x1,x2)
? 输入断言,x>=0∧y>=0∧(x≠0∨y≠0) 可能不能保证整个程序的运
行的正常终止。如 x>0,y=0时,程序会出现什么情况？
部分正确性证明 － 子目标断言法
子目标断言法是在不变式断
言法基础发展起来的一种证明
程序部分正确性的。与不变式
断言法主要区别在于：
（ 1）对循环所建立的断言不同。
不变式断言描述了程序变量 y的
中间值与初值之间的关系，而
子目标断言描述的是 y的中间值
与循环终止时的最终值 yf之间
的关系；
（ 2）进行归纳的方向不同。不变
式断言法沿着程序正常执行的
方向进行归纳，而子目标断言
则沿着相反的方向进行归纳。
例 1设 x,y是非负整数，求它们
的最大公约数，
? z=gcd(x,y)
Program A
? var x,y,z,s:integer;
? begin
? read(x,y);
? while x≠0 do
? if y>=x then y:=y-x
? else
? begin
? s:=x;x:=y;y:=s;
? end
? z:=y;
? write(z);
? end
部分正确性证明 － 子目标断言法实例
(1)建立断言 。 设 x,y的初始值为 x0,y0,
输入断言,Φ(x):x0>=0∧y0>=0∧(x0≠0∨y0≠0)
? 输出断言 Ψ(x,z):z=gcd(x0,y0)
? 在循环断点 L处建立子目标断言 q(x,y,yf)：
? x>=0∧y>=0∧(x≠0∨y≠0) ->yf=gcd(x,y)
? (2)建立检验条件。首先证明当程序控制最后一次通过 L时，及控制转出循
环时，子目标断言应该成立。此时的检验条件为：
检验条件 1：
X=0->[x>=0∧y>=0∧(x≠0∨y≠0) ->yf=gcd(x,y)]
接下来要进一步证明，在循环终止前，子目标断言也应该成立。程序控制
循环再次回到断点 L处有两个途径，一个是 y>=x成立时，另一个是 y<x时。
当 y>=x成立时：
检验条件 2：
［ q(x,y - x,yf)∧x≠0∧y>=x] ->q(x,y,yf)
即通过循环的 then通路之后的子目标断言蕴涵通过此通路之前的子目标断言。
部分正确性证明 － 子目标断言法实例
当 y<x成立时：
检验条件 3：
［ q(y,x,yf)∧x≠0∧y<x] ->q(x,y,yf)
即通过循环的 else通路之后的子目标断言蕴涵通过此通路之前的子目
标断言。
接下来要进一步证明，如果输入断言为真，且当控制第一次通过 L
时子目标断言为真，则输出断言为真，整个反向推理结束。
检验条件 4：
x0>=0∧y0>=0∧(x0≠0∨y0≠0)∧q(x0,y0,yf) ->yf=gcd(x0,y0)
(3)证明检验条件
条件 1：
x=0->[x>=0∧y>=0∧(x≠0∨y≠0) ->yf=gcd(x,y)]
关键点在于 x=0时,yf是否等于 gcd(x,y)？ 退出循环后,yf=y，
gcd(x,y)=gcd(0,yf),根据数论知识,gcd(0,yf)=yf是成立的，即
yf=gcd(x,y)成立。
部分正确性证明 － 子目标断言法实例
条件 2：
［ q(x,y - x,yf)∧x≠0∧y>=x] ->q(x,y,yf),考虑到
q(x,y,yf)为：
? x>=0∧y>=0∧(x≠0∨y≠0) ->yf=gcd(x,y),代入条件 2：
[[x>=0∧y -x>=0∧(x≠0∨y -x≠0) ->yf=gcd(x,y-
x)]∧x≠0∧y>=x] ->
[x>=0∧y>=0∧(x≠0∨y≠0) ->yf=gcd(x,y)]
如果蕴涵式前项成立，存在 x≠0, y>=x为真，则
x>=0∧y>=0∧(x≠0∨y≠0) 为真。 由再根据数论中辗转法可
知,y>=x时,gcd(x,y)=gcd(x,y - x)成立，因此 yf=gcd(x,y)
成立，由此，条件 2为真。
部分正确性证明 － 子目标断言法实例
条件 3：
［ q(y,x,yf)∧x≠0∧y<x] ->q(x,y,yf),考虑到 q(x,y,yf)为：
? x>=0∧y>=0∧(x≠0∨y≠0) ->yf=gcd(x,y),代入条件 3：
[[y>=0∧x>=0∧(y≠0∨x≠0) ->yf=gcd(y,x)]∧x≠0∧y<x] ->
[x>=0∧y>=0∧(x≠0∨y≠0) ->yf=gcd(x,y)]
如果蕴涵式前项成立，由于 x,y互换，由合适公式的互换定律，可以推
导出 x>=0∧y>=0∧(x≠0∨y≠0) 为真，根据数论中辗转法可知
gcd(x,y)= gcd(y,x),由此，条件 3为真。
检验条件 4：
x0>=0∧y0>=0∧(x0≠0∨y0≠0)∧q(x0,y0,yf) ->yf=gcd(x0,y0),考虑
到 q(x0,y0,yf)为：
? x0>=0∧y0>=0∧(x0≠0∨y0≠0) ->yf=gcd(x0,y0),代入条件 4：
[x0>=0∧y0>=0∧(x0≠0∨y0≠0)∧[x0>=0∧y0>=0∧(x0≠0∨y0≠0) -
>yf=gcd(x0,y0)]]->yf=gcd(x0,y0),很显然，条件 4为真。
部分正确性证明 － 子目标断言法实例
根据子目标断言法的定义，证明了：
（ 1）每当控制到达 L时，子目标断言都是成立的；
（ 2）当输入断言为真，且当程序第一次运行到 L时子目标断言
成立，则输出断言为真。
事实上，不论是子目标断言法还是不变式断言法，其关键都
在于建立正确的断言描述。但建立正确的断言环主要依赖程
序设计人员的实践经验，还没有一个有效的、系统的方法。
程序的终止性证明 － 计数器法
计数器法是由 D.E.knuth在 1968年提出来的一种与
不变式断言相配套的程序终止性证明的基本方法。
基本思想：对程序中的每一个循环附加一个计数器
变量，进入循环之前，计数器置为 0，循环通路每执行
一次，计数器加 1。同时，对每一个循环提供一个新的
中间断言，用来表示相应的计数器不会超过某个固定的
界限。然后，证明此中间断言是不变式断言，就可以断
定循环只能执行有限次，因而程序是终止的。
程序的终止性证明 － 计数器法实例
例 1：用计数器法证明程序的终止性
? 设 x,y是非负整数，求它们的最大公约数，
? z=gcd(x,y)
? Program A
? var x,y,z,s:integer;
? begin
? read(x,y);
? while x≠0 do
? if y>=x then y:=y-x
? else
? begin
? s:=x;x:=y;y:=s;
? end
? z:=y;
? write(z);
? End
程序的终止性证明 － 计数器法实例
建立输入断言,Φ(x):x0>=0∧y0>=0∧(x0≠0∨y0≠0)
? （ 1）建立计数器 I及其中间断言, x>=0∧y>=0∧2x+y+i<=2x0+y0
? 考虑到输入断言,x0>=0∧y0>=0∧(x0≠0∨y0≠0), 可以推断 i的上限
不能超过 2x0+y0
? 将断言直接写入程序中（ 这段代码中，计数器 i的设置有问题,请大家
? Program A 思考该如何修改？ ）
? var x,y,z,s:integer;
? begin
? read(x,y);
? ｛ x0>=0∧y0>=0∧(x0≠0∨y0≠0) ｝ //输入断言
? while x≠0 do
? L：｛ x>=0∧y>=0∧2x+y+i<=2x0+y0 ｝ //计数器断言
? if y>=x then y:=y-x
? else
? begin
? s:=x;x:=y;y:=s;i:=i+1;
? end
? z:=y;
? write(z);
? End
程序的终止性证明 － 计数器法实例
（ 2）建立检验条件。设 x,y的初始值为 x0,y0,假定输入断言成立，即要证明
程序第一次执行到断点 L处时，中间断言成立。此时,x=x0,y=y0,i=0,检
验条件为：
检验条件 1：
［ x0>=0∧y0>=0∧(x0≠0∨y0≠0)] ->[x0>=0∧y0>=0∧(2x0+y0<=2x0+y0)]
进一步证明，当检验条件 1成立，程序控制循环再次回到计数器断点 L
处时，中间断言仍然成立。程序控制循环再次回到断点 L处有两个途径，
一个是 y>=x成立时，另一个是 y<x时。当 y>=x成立时：
检验条件 2：
［ x>=0∧y>=0∧(2x+y+i<=2x0+y0)∧(x≠0∧y>=x)] ->[x>=0∧y -x>=0
∧(2x+y -x+i+1<=2x0+y0)]
当 y<x成立时：
检验条件 3：
［ x>=0∧y>=0∧(2x+y+i<=2x0+y0)∧(x≠0∧y<x)] ->[y>=0∧x>=0
∧(2y+x+i+1<=2x0+y0)]
程序的终止性证明 － 计数器法实例
(3)证明检验条件
条件 1：程序第一次执行到 L处时,(2x0+y0<=2x0+y0)成立，整个检
验条件 1成立。
条件 2：如果蕴涵式前项成立，由 x>=0,y>=x成立可以推导出：
x>=0∧y -x>=0成立。而,2x+y-x+i+1=2x+y+i+1-x,由于
x>=0∧x≠0, 推出,1-x<=0,
2x+y-x+i+1=2x+y+i+1-x<=2x+y+i<=2x0+y0成立
由此，条件 2为真。
条件 3：如果蕴涵式前项成立，由于 x,y互换,关键是要证明
(2y+x+i+1<=2x0+y0)为真。由于：
2y+x+i+1=2x+y+i+y-x+1=2x+y+i+y-(x-1)
由于 y<x,且 x,y为自然数，存在,y<=x-1
因此,2y+x+i+1=2x+y+i+y-x+1=2x+y+i+y-(x-1)<= 2x+y+i<=2x0+y0成立
由此，条件 3为真。整个程序的终止性得以证明。
程序的终止性证明 － 计数器法实例
(4)显然，由于不论以何种方式通过循环通路时，中间断
言都成立，也即此时的中间断言是不变式断言，
2x+y+i<=2x0+y0恒为真，考虑到 x>=0,y>=0,存在
2x+y>0,必定存在,i<2x0+y0
也即循环计数器存在一个上限 (2x0+y0) 。循环只能执
行有限次，程序是可以终止的。
程序的终止性证明 － 计数器法实例
计数器方法的另一种形式：
对程序中的每一个循环，构造一个和该循环中变量相
关的有界正整函数 N(x,y),若 N(x,y)满足下面两
个条件：
(1)当使循环继续进行的条件成立时,N(x,y)>0
(2)每执行一次循环,N(x,y)的值都减小
则可以证明程序的终止性。
? 例 2：设 x1,x2是正整数，求它们的最大公约数，
? z=gcd(x1,x2)
选择 N(y1,y2)=max(y1,y2),设输入断言为：
? 输入断言 Φ(x):x1>0∧x2>0
程序的终止性证明 － 计数器法实例
程序第一次进入循环时：
y1>0∧y2>0,再根据循环体中的基本算法
? 对于任意正整数 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
可以推导出：在循环进行时，始终有：
y1>0∧y2>0 成立
由此：
(1)N(y1,y2)=max(y1,y2)>0,且 N(y1,y2)=max(y1,y2)<=
max(x1,x2)是有界的；
(2)每执行一次循环,有两种途径,y1>y2时,y1=y1-y2,y2=y2,
可以推导出,N(y1-y2,y2)<N(y1,y2)
因此：对任何满足输入断言 Φ(x)的 x1和 x2,程序都是终止的。
程序的终止性证明
小结：
(1)利用计数器方法证明程序终止性的主要困难在于
确定一个合适的中间断言或选取一个合适的中间断
点函数 N(x,y)。 特别是对于一些循环次数事先难于
估计的程序，要确定循环次数的上限就更为困难。
(2)利用计数器方法证明程序终止性和利用不变式断
言证明程序的部分正确性的过程是类似的。可以将
两者结合，实现程序的完全性证明。
程序正确性证明
本章主要研究内容
? 基本概念
? 程序测试的基本方法
? 部分正确性证明方法
? 终止性证明方法
基本概念－ 程序正确性的定义
? 一段程序是正确的，是指这段程序能正确无误地完成程
序设计时所期望的功能。或者说：对任何一组允许的输入信
息，程序执行后能得到一组和这组输入信息相对应的正确的
输出信息。程序的正确性是衡量一个程序是否优秀的最基本
条件。
? 一段程序是错误的，是指（ 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
? 试测试下面这一程序
? Procedure P(var A,B:REAL)
? Begin
? If(A > 1)and(B = 0) then X:=X/A;
? If(A=2)or(X>1)then X:=X+1;
? end
测试用例举例
? 在执行这个程序时，
有各种不同的路径，
如：
? a b d
? a b e d
? a c b d
? a c b e d
测试用例举例
? 我们可用白盒子方法设计测试用例，其任务是
尽可能多地执行各种语句，以及调试到各种路
径。
? 如选择 A = 2,B = 0,X = 3
? 则可执行路径
? a c b e d
? 此时能覆盖到全部 2个计算框，可发现一般的语句
的错误
? 我们通常把这种注重语句的复盖叫, 语句复盖,
测试用例举例
? 如选择
? A = 3,B = 0,X = 1
? A = 2,B = 1,X = 3
? 则可执行的路径为
? a c b d
? a b e d
? 从所走路径来看，上面这组数据要全面一些，它不仅通过
全部两个计算框，而且第一个判别框的两边都执行过一次。
? 我们通常把这种注重选择测试的复盖叫做, 判定复盖,
程序测试
? 从以上两个例子可以看出，测试通常是
不充分的，它只能发现某些错误的存在，
而不能证明错误的不存在。
? 所有，在真正设计测试用例的过程种常
常要考虑经济性，可行性。
? 测试的关键就是如何设计好高效，可行
的用例程序。
程序测试
? 如选择
? A=2,B=0,X=4
? A=1,B=1,X=1
? 则可执行的路径为
? a c b e d
? a b d
? 从这组数据来看，它注意了 4个条件
A>1,B=0,A=2和 X>1的复盖。我们称这种注重判
断的复盖为, 条件复盖,
程序测试
? 以上这些数据虽然均达到一些测试目的，且各有侧重，但是都是
不充分的。
? 如从条件出发，用组合的办法使各个条件都能执行到，则我们可
以写出以下 8种条件组合：
? 1)A>1,B=0
? 2)A>1,B<>0;(<>是不等号 )
? 3)A<=1,B=0
? 4)A<=1,B<>0
? 5)A=2,X>1
? 6)A=2,X<=1
? 7)A<>2,X>1
? 8)A<>2,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
? 它们都能使各种条件均能出现一次。虽然这个组合
方法比较方便，逻辑也很清楚，且对执行条件来说
还是比较全面的，但是仍然又未走遍的路径，如 a c
b d
程序测试
? 在测试时，还
要注意到计算
机执行多个条
件的特点，即
它必须把多个
条件分解为简
单判别才能执
行，如上述例
子可分解为右
图。
例子 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和 QuickTest Professional作为自动化测试工
具, 推荐 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)∧R i(x,y)－ >Ψi(x,ri(x,y))
? （ 3）证明检验条件，即证明（ 2）中所列出的所有检验条件，
如果每一条通路上的检验条件都为真，则该程序是部分正确
的。
部分正确性证明 － 不变式断言法实例
? 例 1：设 x1,x2是正整数，求它们的最大公约数，
? z=gcd(x1,x2)
? 基本算法：对于任意正整数 x1,x2,有：
? （ 1）若 x1>x2,gcd(x1,x2)=gcd(x1-x2,x2)
? （ 2）若 x2>x1,gcd(x1,x2)=gcd(x1,x2-x1)
? （ 3）若 x1=x2,gcd(x1,x2)=x1=x2
? 即反复执行（ 1）或（ 2），直到出现（ 3）中的情况
部分正确性证明 － 不变式断言法实例
(x1,x2)->(y1,y2)
y1=y2
开始
y1>y2
y1 ->z
结束
y2-y1->y2y1-y2->y1
B······ P(x,y)
A······ Φ(x)
T
G
C······ Ψ(x,z)
F
ED
F
T
部分正确性证明 － 不变式断言法实例
? 利用不变式断言法实例证明该流程框图的部分正确性,
? (1) 建立断言
? 输入断言 Φ(x):x1>0∧x2>0
? 输出断言 Ψ(x,z):z=gcd(x1,x2)
? 考虑到存在循环，将循环在 B点断开，建立 B点的不变式断言：
? P(x,y):x1>0∧x2>0∧y1>0∧y2>0∧gcd(y1,y2)=gcd(x1,x2)
? 其中,x,y分别表示 (x1,x2),(y1,y2)。
? (2) 建立检验条件
? 将 B设为断点后，程序执行中所有可能的通路分解为：
? 通路 1,A->B
? 通路 2,B->D->B
? 通路 3,B->E->B
? 通路 4,B->G->C
部分正确性证明 － 不变式断言法实例
? 利用不变式断言法实例证明该流程框图的部分正确性,
? (1) 建立断言
? 输入断言 Φ(x):x1>0∧x2>0
? 输出断言 Ψ(x,z):z=gcd(x1,x2)
? 考虑到存在循环，将循环在 B点断开，建立 B点的不变式断言：
? P(x,y):x1>0∧x2>0∧y1>0∧y2>0∧gcd(y1,y2)=gcd(x1,x2)
? 其中,x,y分别表示 (x1,x2),(y1,y2)。
? (2) 建立检验条件
? 通路 1的检验条件, 通路 1（ A->B） 是无条件的,
? 即 R1(x,y)=1（恒为真），同时 Φ1(x)－ > P(x,y),具体可写为：
? ［ x1>0∧x2>0] ->[x1>0∧x2>0∧y1>0∧y2>0∧gcd(y1,y2)=gcd(x1,x2)]
部分正确性证明 － 不变式断言法实例
? 通路 2的检验条件, R2(x,y)=[y1≠y2 ∧y1>y2>],通路 2的输入、输出
断言均为,P(x,y),因而检验条件为：
? ［ P(x,y)∧y1≠y2∧y1>y2>] ->P(x,y1-y2,y2),也即：
? [x1>0∧x2>0∧y1>0∧y2>0∧gcd(y1,y2)=gcd(x1,x2)
∧y1≠y2∧y1>y2] ->[x1>0∧x2>0∧(y1 -y2)>0∧y2>0∧gcd(y1 -
y2,y2)=gcd(x1,x2)]
? 通路 3的检验条件, R3(x,y)=[y1≠y2 ∧y1<y2>],通路 3的输入、输出
断言均为,P(x,y),因而检验条件为：
? ［ P(x,y)∧y1≠y2∧y1<y2>] ->P(x,y1,y2-y1),也即：
? [x1>0∧x2>0∧y1>0∧y2>0∧gcd(y1,y2)=gcd(x1,x2)
∧y1≠y2∧y1<y2] ->[x1>0∧x2>0∧y1>0∧(y2 -y1)>0∧gcd(y1,y2 -
y1)=gcd(x1,x2)]
? 通路 4的检验条件, R4(x,y)=[y1=y2],通路 4的输入断言为 P(x,y),
输出断言为 Ψ(x1,y2),检验条件为：
? ［ P(x,y)∧y1=y2] ->Ψ(x1,y2)
考试时间
?下周四晚 7,00------9,30
?地点西 12 S401到 S404,S406到
S412
?周五上课时间、地点不变
部分正确性证明 － 不变式断言法实例
? （ 3）证明检验条件是否成立
? 通路 1、通路 4的检验条件为真
? 对于 通路 2，检验条件为：
? [x1>0∧x2>0∧y1>0∧y2>0∧gcd(y1,y2)=gcd(x1,x2)
∧y1≠y2∧y1>y2] ->[x1>0∧x2>0∧(y1 -y2)>0∧y2>0∧gcd(y1 -
y2,y2)=gcd(x1,x2)]
? 检验条件的前项为真（成立）时,[y1>y2]->[y1-y2>0],更求最
大公约数的辗转算法,gcd(y1-y2,y2)=gcd(y1,y2)=gcd(x1,x2)，
此时,检验条件的后项为真（成立），因此，整个蕴涵运算为真，
即检验条件为真。
? 同理可证条件 3成立。
? 整个流程图的部分正确性得到了证明。
部分正确性证明 － 不变式断言法实例
不变式断言法也可以直接用于高级语言写出的程序。具体使用时，
以注释的形式在程序的断点处加上断言。
? 例 2：设 x,y是非负整数，求它们的最大公约数，
? z=gcd(x,y)
? Program A
? var x,y,z,s:integer;
? begin
? read(x,y);
? while x≠0 do
? if y>=x then y:=y-x
? else
? begin
? s:=x;x:=y;y:=s;
? end
? z:=y;
? write(z);
? end
部分正确性证明 － 不变式断言法实例
(1)建立断言 。 设 x,y的初始值为 x0,y0,
输入断言,Φ(x):x0>=0∧y0>=0∧(x0≠0∨y0≠0)
? 输出断言 Ψ(x,z):z=gcd(x0,y0)
? 不变式断言：
? P(x,y):x>=0∧y>=0∧(x0≠0∨y0≠0)∧gcd(x,y)=gcd(x0,y0)
? 将断言直接写入程序中：
? Program A
? var x,y,z,s:integer;
? begin
? read(x,y);
? ｛ x0>=0∧y0>=0∧(x0≠0∨y0≠0) ｝ //输入断言
? while x≠0 do
? L：｛ x>=0∧y>=0∧(x0≠0∨y0≠0)∧gcd(x,y)=gcd(x0,y0) ｝ //不变式断言
? if y>=x then y:=y-x
? else
? begin
? s:=x;x:=y;y:=s;
? end
? z:=y;
? {z=gcd(x0,y0)} //输出断言
? write(z);
? end
部分正确性证明 － 不变式断言法实例
(2)建立检验条件。设 x,y的初始值为 x0,y0,假定输入断言成立，即要证明
程序第一次执行到断点 L处时，不变式断言成立。此时的检验条件为：
检验条件 1：
［ x0>=0∧y0>=0∧(x0≠0∨y0≠0)] ->
[x0>=0∧y0>=0∧(x0≠0∨y0≠0)∧gcd(x,y)=gcd(x0,y0)]
进一步证明，当检验条件 1成立，程序控制循环后再次回到断点 L处时，不
变式断言仍然成立。程序控制循环再次回到断点 L处有两个途径，一个
是 y>=x成立时，另一个是 y<x时。当 y>=x成立时：
检验条件 2：
［ x>=0∧y>=0∧(x≠0∨y≠0)∧gcd(x,y)=gcd(x0,y0)∧x≠0∧y>=x] -
>[x>=0∧y -x>=0∧(x≠0∨y - x≠0)∧gcd(x,y - x)=gcd(x0,y0)]
当 y<x成立时：
检验条件 3：
［ x>=0∧y>=0∧(x≠0∨y≠0)∧gcd(x,y)=gcd(x0,y0)∧x≠0∧y<x] -
>[y>=0∧x>=0∧(y≠0∨x≠0)∧gcd(y,x)=gcd(x0,y0)]
部分正确性证明 － 不变式断言法实例
最后要证明如果不变时断言成立，但程序控制转出循环时，输出断言
成立。此时的检验条件为：
检验条件 4：
［ x>=0∧y>=0∧(x≠0∨y≠0)∧gcd(x,y)=gcd(x0,y0)∧x=0] -
>y=gcd(x0,y0)
(3)证明检验条件
条件 1：程序第一次执行到 L处时,x=x0,y=y0,gcd(x,y)=gcd(x0,y0)
成立，整个检验条件 1成立。
条件 2：如果蕴涵式前项成立，由 x>=0,y>=x成立可以推导出：
x>=0∧y -x>=0成立。由 x≠0 成立可以推导出,x≠0∨y - x≠0 成
立,再根据数论中辗转法可知,y>=x时,gcd(x,y)=gcd(x,y - x)
成立，而 gcd(x,y)=gcd(x0,y0)成立，因此 gcd(x,y -
x)=gcd(x0,y0)成立，由此，条件 2为真。
条件 3：如果蕴涵式前项成立，由 x,y互换，由合适公式的互换定律，
可以推导出条件 2为真。
部分正确性证明 － 不变式断言法实例
条件 4：如果蕴涵式前项成立，由
x>=0∧y>=0∧(x≠0∨y≠0)∧gcd(x,y)=gcd(x0,y0)∧x=0 可以推出
x=0,再由 (x≠0∨y≠0) 成立可以推导出 y>0 。再根据数论中辗转法
可知,x=0,y>0时,gcd(0,y)=y成立，由此，条件 4为真。
整个程序的部分正确性得以证明。
整个程序的部分正确性不能保证整个程序的完全正确性。
在例 1中，若将问题前提改为与例 2一致：设 x1,x2是非负整数，求它
们的最大公约数,z=gcd(x1,x2)
? 输入断言,x>=0∧y>=0∧(x≠0∨y≠0) 可能不能保证整个程序的运
行的正常终止。如 x>0,y=0时,程序会出现什么情况？
部分正确性证明 － 子目标断言法
子目标断言法是在不变式断
言法基础发展起来的一种证明
程序部分正确性的。与不变式
断言法主要区别在于：
（ 1）对循环所建立的断言不同。
不变式断言描述了程序变量 y的
中间值与初值之间的关系，而
子目标断言描述的是 y的中间值
与循环终止时的最终值 yf之间
的关系；
（ 2）进行归纳的方向不同。不变
式断言法沿着程序正常执行的
方向进行归纳，而子目标断言
则沿着相反的方向进行归纳。
例 1设 x,y是非负整数，求它们
的最大公约数，
? z=gcd(x,y)
Program A
? var x,y,z,s:integer;
? begin
? read(x,y);
? while x≠0 do
? if y>=x then y:=y-x
? else
? begin
? s:=x;x:=y;y:=s;
? end
? z:=y;
? write(z);
? end
部分正确性证明 － 子目标断言法实例
(1)建立断言 。 设 x,y的初始值为 x0,y0,
输入断言,Φ(x):x0>=0∧y0>=0∧(x0≠0∨y0≠0)
? 输出断言 Ψ(x,z):z=gcd(x0,y0)
? 在循环断点 L处建立子目标断言 q(x,y,yf)：
? x>=0∧y>=0∧(x≠0∨y≠0) ->yf=gcd(x,y)
? (2)建立检验条件。首先证明当程序控制最后一次通过 L时，及控制转出循
环时，子目标断言应该成立。此时的检验条件为：
检验条件 1：
X=0->[x>=0∧y>=0∧(x≠0∨y≠0) ->yf=gcd(x,y)]
接下来要进一步证明，在循环终止前，子目标断言也应该成立。程序控制
循环再次回到断点 L处有两个途径，一个是 y>=x成立时，另一个是 y<x时。
当 y>=x成立时：
检验条件 2：
［ q(x,y - x,yf)∧x≠0∧y>=x] ->q(x,y,yf)
即通过循环的 then通路之后的子目标断言蕴涵通过此通路之前的子目标断言。
部分正确性证明 － 子目标断言法实例
当 y<x成立时：
检验条件 3：
［ q(y,x,yf)∧x≠0∧y<x] ->q(x,y,yf)
即通过循环的 else通路之后的子目标断言蕴涵通过此通路之前的子目
标断言。
接下来要进一步证明，如果输入断言为真，且当控制第一次通过 L
时子目标断言为真，则输出断言为真，整个反向推理结束。
检验条件 4：
x0>=0∧y0>=0∧(x0≠0∨y0≠0)∧q(x0,y0,yf) ->yf=gcd(x0,y0)
(3)证明检验条件
条件 1：
x=0->[x>=0∧y>=0∧(x≠0∨y≠0) ->yf=gcd(x,y)]
关键点在于 x=0时,yf是否等于 gcd(x,y)？ 退出循环后,yf=y，
gcd(x,y)=gcd(0,yf),根据数论知识,gcd(0,yf)=yf是成立的，即
yf=gcd(x,y)成立。
部分正确性证明 － 子目标断言法实例
条件 2：
［ q(x,y - x,yf)∧x≠0∧y>=x] ->q(x,y,yf),考虑到
q(x,y,yf)为：
? x>=0∧y>=0∧(x≠0∨y≠0) ->yf=gcd(x,y),代入条件 2：
[[x>=0∧y -x>=0∧(x≠0∨y -x≠0) ->yf=gcd(x,y-
x)]∧x≠0∧y>=x] ->
[x>=0∧y>=0∧(x≠0∨y≠0) ->yf=gcd(x,y)]
如果蕴涵式前项成立，存在 x≠0, y>=x为真，则
x>=0∧y>=0∧(x≠0∨y≠0) 为真。 由再根据数论中辗转法可
知,y>=x时,gcd(x,y)=gcd(x,y - x)成立，因此 yf=gcd(x,y)
成立，由此，条件 2为真。
部分正确性证明 － 子目标断言法实例
条件 3：
［ q(y,x,yf)∧x≠0∧y<x] ->q(x,y,yf),考虑到 q(x,y,yf)为：
? x>=0∧y>=0∧(x≠0∨y≠0) ->yf=gcd(x,y),代入条件 3：
[[y>=0∧x>=0∧(y≠0∨x≠0) ->yf=gcd(y,x)]∧x≠0∧y<x] ->
[x>=0∧y>=0∧(x≠0∨y≠0) ->yf=gcd(x,y)]
如果蕴涵式前项成立，由于 x,y互换，由合适公式的互换定律，可以推
导出 x>=0∧y>=0∧(x≠0∨y≠0) 为真，根据数论中辗转法可知
gcd(x,y)= gcd(y,x),由此，条件 3为真。
检验条件 4：
x0>=0∧y0>=0∧(x0≠0∨y0≠0)∧q(x0,y0,yf) ->yf=gcd(x0,y0),考虑
到 q(x0,y0,yf)为：
? x0>=0∧y0>=0∧(x0≠0∨y0≠0) ->yf=gcd(x0,y0),代入条件 4：
[x0>=0∧y0>=0∧(x0≠0∨y0≠0)∧[x0>=0∧y0>=0∧(x0≠0∨y0≠0) -
>yf=gcd(x0,y0)]]->yf=gcd(x0,y0),很显然，条件 4为真。
部分正确性证明 － 子目标断言法实例
根据子目标断言法的定义，证明了：
（ 1）每当控制到达 L时，子目标断言都是成立的；
（ 2）当输入断言为真，且当程序第一次运行到 L时子目标断言
成立，则输出断言为真。
事实上，不论是子目标断言法还是不变式断言法，其关键都
在于建立正确的断言描述。但建立正确的断言环主要依赖程
序设计人员的实践经验，还没有一个有效的、系统的方法。
程序的终止性证明 － 计数器法
计数器法是由 D.E.knuth在 1968年提出来的一种与
不变式断言相配套的程序终止性证明的基本方法。
基本思想：对程序中的每一个循环附加一个计数器
变量，进入循环之前，计数器置为 0，循环通路每执行
一次，计数器加 1。同时，对每一个循环提供一个新的
中间断言，用来表示相应的计数器不会超过某个固定的
界限。然后，证明此中间断言是不变式断言，就可以断
定循环只能执行有限次，因而程序是终止的。
程序的终止性证明 － 计数器法实例
例 1：用计数器法证明程序的终止性
? 设 x,y是非负整数，求它们的最大公约数，
? z=gcd(x,y)
? Program A
? var x,y,z,s:integer;
? begin
? read(x,y);
? while x≠0 do
? if y>=x then y:=y-x
? else
? begin
? s:=x;x:=y;y:=s;
? end
? z:=y;
? write(z);
? End
程序的终止性证明 － 计数器法实例
建立输入断言,Φ(x):x0>=0∧y0>=0∧(x0≠0∨y0≠0)
? （ 1）建立计数器 I及其中间断言, x>=0∧y>=0∧2x+y+i<=2x0+y0
? 考虑到输入断言,x0>=0∧y0>=0∧(x0≠0∨y0≠0), 可以推断 i的上限
不能超过 2x0+y0
? 将断言直接写入程序中（ 这段代码中，计数器 i的设置有问题,请大家
? Program A 思考该如何修改？ ）
? var x,y,z,s:integer;
? begin
? read(x,y);
? ｛ x0>=0∧y0>=0∧(x0≠0∨y0≠0) ｝ //输入断言
? while x≠0 do
? L：｛ x>=0∧y>=0∧2x+y+i<=2x0+y0 ｝ //计数器断言
? if y>=x then y:=y-x
? else
? begin
? s:=x;x:=y;y:=s;i:=i+1;
? end
? z:=y;
? write(z);
? End
程序的终止性证明 － 计数器法实例
（ 2）建立检验条件。设 x,y的初始值为 x0,y0,假定输入断言成立，即要证明
程序第一次执行到断点 L处时，中间断言成立。此时,x=x0,y=y0,i=0,检
验条件为：
检验条件 1：
［ x0>=0∧y0>=0∧(x0≠0∨y0≠0)] ->[x0>=0∧y0>=0∧(2x0+y0<=2x0+y0)]
进一步证明，当检验条件 1成立，程序控制循环再次回到计数器断点 L
处时，中间断言仍然成立。程序控制循环再次回到断点 L处有两个途径，
一个是 y>=x成立时，另一个是 y<x时。当 y>=x成立时：
检验条件 2：
［ x>=0∧y>=0∧(2x+y+i<=2x0+y0)∧(x≠0∧y>=x)] ->[x>=0∧y -x>=0
∧(2x+y -x+i+1<=2x0+y0)]
当 y<x成立时：
检验条件 3：
［ x>=0∧y>=0∧(2x+y+i<=2x0+y0)∧(x≠0∧y<x)] ->[y>=0∧x>=0
∧(2y+x+i+1<=2x0+y0)]
程序的终止性证明 － 计数器法实例
(3)证明检验条件
条件 1：程序第一次执行到 L处时,(2x0+y0<=2x0+y0)成立，整个检
验条件 1成立。
条件 2：如果蕴涵式前项成立，由 x>=0,y>=x成立可以推导出：
x>=0∧y -x>=0成立。而,2x+y-x+i+1=2x+y+i+1-x,由于
x>=0∧x≠0, 推出,1-x<=0,
2x+y-x+i+1=2x+y+i+1-x<=2x+y+i<=2x0+y0成立
由此，条件 2为真。
条件 3：如果蕴涵式前项成立，由于 x,y互换,关键是要证明
(2y+x+i+1<=2x0+y0)为真。由于：
2y+x+i+1=2x+y+i+y-x+1=2x+y+i+y-(x-1)
由于 y<x,且 x,y为自然数，存在,y<=x-1
因此,2y+x+i+1=2x+y+i+y-x+1=2x+y+i+y-(x-1)<= 2x+y+i<=2x0+y0成立
由此，条件 3为真。整个程序的终止性得以证明。
程序的终止性证明 － 计数器法实例
(4)显然，由于不论以何种方式通过循环通路时，中间断
言都成立，也即此时的中间断言是不变式断言，
2x+y+i<=2x0+y0恒为真，考虑到 x>=0,y>=0,存在
2x+y>0,必定存在,i<2x0+y0
也即循环计数器存在一个上限 (2x0+y0) 。循环只能执
行有限次，程序是可以终止的。
程序的终止性证明 － 计数器法实例
计数器方法的另一种形式：
对程序中的每一个循环，构造一个和该循环中变量相
关的有界正整函数 N(x,y),若 N(x,y)满足下面两
个条件：
(1)当使循环继续进行的条件成立时,N(x,y)>0
(2)每执行一次循环,N(x,y)的值都减小
则可以证明程序的终止性。
? 例 2：设 x1,x2是正整数，求它们的最大公约数，
? z=gcd(x1,x2)
选择 N(y1,y2)=max(y1,y2),设输入断言为：
? 输入断言 Φ(x):x1>0∧x2>0
程序的终止性证明 － 计数器法实例
程序第一次进入循环时：
y1>0∧y2>0,再根据循环体中的基本算法
? 对于任意正整数 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
可以推导出：在循环进行时，始终有：
y1>0∧y2>0 成立
由此：
(1)N(y1,y2)=max(y1,y2)>0,且 N(y1,y2)=max(y1,y2)<=
max(x1,x2)是有界的；
(2)每执行一次循环,有两种途径,y1>y2时,y1=y1-y2,y2=y2,
可以推导出,N(y1-y2,y2)<N(y1,y2)
因此：对任何满足输入断言 Φ(x)的 x1和 x2,程序都是终止的。
程序的终止性证明
小结：
(1)利用计数器方法证明程序终止性的主要困难在于
确定一个合适的中间断言或选取一个合适的中间断
点函数 N(x,y)。 特别是对于一些循环次数事先难于
估计的程序，要确定循环次数的上限就更为困难。
(2)利用计数器方法证明程序终止性和利用不变式断
言证明程序的部分正确性的过程是类似的。可以将
两者结合，实现程序的完全性证明。
