程序正确性证明课件

程序正确性证明

基本概念－程序正确性的定义

一段程序是正确的，是指这段程序能正确无误地完成程序设计时所期望的功能。或者说：对任何一组允许的输入信息，程序执行后能得到一组和这组输入信息相对应的正确的输出信息。程序的正确性是衡量一个程序是否优秀的最基本条件。一段程序是错误的，是指（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试测试下面这一程序ProcedureP(varA,B:REAL)BeginIf(A>1)and(B=0)thenX:=X/A;If(A=2)or(X>1)thenX:=X+1;end测试用例举例在执行这个程序时，有各种不同的路径，如：abdabedacbdacbed测试用例举例我们可用白盒子方法设计测试用例，其任务是尽可能多地执行各种语句，以及调试到各种路径。如选择A=2,B=0,X=3则可执行路径acbed此时能覆盖到全部2个计算框，可发现一般的语句的错误我们通常把这种注重语句的复盖叫“语句复盖”测试用例举例如选择A=3,B=0,X=1A=2,B=1,X=3则可执行的路径为acbdabed从所走路径来看，上面这组数据要全面一些，它不仅通过全部两个计算框，而且第一个判别框的两边都执行过一次。我们通常把这种注重选择测试的复盖叫做“判定复盖”程序测试从以上两个例子可以看出，测试通常是不充分的，它只能发现某些错误的存在，而不能证明错误的不存在。所有，在真正设计测试用例的过程种常常要考虑经济性，可行性。测试的关键就是如何设计好高效，可行的用例程序。程序测试如选择A=2,B=0,X=4A=1,B=1,X=1则可执行的路径为

acbedabd从这组数据来看，它注意了4个条件A>1,B=0,A=2和X>1的复盖。我们称这种注重判断的复盖为“条件复盖”程序测试以上这些数据虽然均达到一些测试目的，且各有侧重，但是都是不充分的。如从条件出发，用组合的办法使各个条件都能执行到，则我们可以写出以下8种条件组合：1)A>1,B=02)A>1,B<>0;(<>是不等号)3)A<=1,B=04)A<=1,B<>05)A=2,X>16)A=2,X<=17)A<>2,X>18)A<>2,X<=1程序测试根据这8种条件组合，又可以优化组成如下4组数据：A=2,B=0,X=4A=2,B=1,X=1A=1,B=0,X=2A=1,B=1,X=1它们都能使各种条件均能出现一次。虽然这个组合方法比较方便，逻辑也很清楚，且对执行条件来说还是比较全面的，但是仍然又未走遍的路径，如acbd程序测试在测试时，还要注意到计算机执行多个条件的特点，即它必须把多个条件分解为简单判别才能执行，如上述例子可分解为右图。例子2某个TRIANGLE程序，用3个整数表示一个三角形的3条边长。当输入3个整数后，该程序输出一个结果，指出这三角形是等腰，等边，还是不等边三角形。程序测试这个例子只知程序的功能，而不知内部的逻辑与结构。在选择数据组来测试程序时，我们可以凭经验，考虑如下情况：1）合理构成等腰三角形2）合理构成等边三角形3）合理构成不等边三角形4）等腰三角形的三种排列5）三个正数，其中两个数之和等于第三个数6）两边之和等于第三边的三种排列7）三个正数，其中两个数之和小于第三个数8）两边之和小于第三边的三种排列程序测试9）输入三个数，其中含有010）输入三个数，其中含有负数11）输入三个数，其中含有非整数值12）输入三个均为0的数13）输入三个均为非法字符列出各种产生的情况来测试的方法显然是黑盒子方法。它不关心盒子内程序的具体逻辑，只是根据程序功能来设计测试用例常用的测试数据选择方法有等价分类法，边缘值分析法，因果图方法和错误推测法等。程序测试等价分类法：根据程序功能将输入的数据划分为若干个等价类，然后考虑数据选择，设计出测试用例。如上例中，我们可将输入条件划分为三种三角形或划分为合理三角形，不合理三角形等二项。在选择时要同时考虑合法的和不合法的数据。有时，还要凭经验和其他知识进行更全面的测试划分。程序测试程序出错通常发生在边界状态，所以在测试中我们常常首先根据程序的功能确定边缘情况的数据变化，以便设计测试用例。对边界状态进行分析，以设计测试用例来测试程序的方法称为边缘值分析法。边缘值的选择要根据题目实际情况有针对性地，有一定创造性地进行。边缘值分析法可以考虑如下几种情况：1）恰好在边界附近，且欲越界的数据2）取最大或最小值，最多或最少值加减1的数据3）循环或迭代的初始值和终值数据4）有序集合的第一个或最后一个数据元素5）零点附近的数据6）最大误差值的数据7）文件处理时的“空文件”，“nil”，”first”等数据程序测试总之，程序测试的黑盒子方法常凭经验进行，在设计测试用例时可以综合使用上述各种方法。在设计测试数据时，我们应该考虑认为最易出错和最易忽略的地方，进行重点测试。程序测试设计测试用例的几点原则：1）测试用例的设计者最好和程序设计者不是同一个人2）对输入的数据欲输出的数据要有详细的了解与描述3）测试用例数据复盖面尽可能大4）测试时既应注意程序是否做了它预定的事，又应该注意检查它不应该做的事5）设计测试用例时要考虑经济性和可行性。程序测试美国MI公司开发的TestDirector产品作为测试管理流程平台，运用WinRunner和QuickTestProfessional作为自动化测试工具，推荐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)∧Ri(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>y2y1->z结束y2-y1->y2y1-y2->y1B······

P(x,y)A······

Φ(x)TGC······

Ψ(x,z)FEDFT部分正确性证明－不变式断言法实例利用不变式断言法实例证明该流程框图的部分正确性:(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地点西12S401到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)ProgramAvarx,y,z,s:integer;beginread(x,y);whilex≠0doify>=xtheny:=y-xelsebegins:=x;x:=y;y:=s;endz:=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)将断言直接写入程序中：ProgramAvarx,y,z,s:integer;beginread(x,y);｛x0>=0∧y0>=0∧(x0≠0∨y0≠0)｝//输入断言whilex≠0doL：｛x>=0∧y>=0∧(x0≠0∨y0≠0)∧gcd(x,y)=gcd(x0,y0)｝//不变式断言ify>=xtheny:=y-xelsebegins:=x;x:=y;y:=s;endz:=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)

ProgramAvarx,y,z,s:integer;beginread(x,y);whilex≠0doify>=xtheny:=y-xelsebegins:=x;x:=y;y:=s;endz:=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)ProgramAvarx,y,z,s:integer;beginread(x,y);whilex≠0doify>=xtheny:=y-xelsebegins:=x;x:=y;y:=s;endz:=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的设置有问题,请大家ProgramA

思考该如何修改？）varx,y,z,s:integer;beginread(x,y);｛x0>=0∧y0>=0∧(x0≠0∨y0≠0)｝//输入断言whilex≠0doL：｛x>=0∧y>=0∧2x+y+i<=2x0+y0｝//计数器断言ify>=xtheny:=y-xelsebegins:=x;x:=y;y:=s;i:=i+1;endz:=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+