程序设计方法学-第三章-程序正确性证明课件

7/14/2024西南石油大学计算机科学学院西南石油大学计算机科学学院西南石油大学计算机科学学院西南石油大学计算机科学学院1第三章 程序正确性证明7/14/2024西南石油大学计算机科学学院西南石油大学计算机科学学院西南石油大学计算机科学学院西南石油大学计算机科学学院2 什么样的程序才是正确的？什么样的程序才是正确的？什么样的程序才是正确的？什么样的程序才是正确的？如何来保证程序是正确的？如何来保证程序是正确的？程序正确性概述7/14/2024西南石油大学计算机科学学院西南石油大学计算机科学学院西南石油大学计算机科学学院西南石油大学计算机科学学院3关于程序正确性的认识 根据问题的特性和软件所要实现的 功能，选择一些具有代表性的数据，设计测试用例。通过用例程序执行，去发现被测试程序的错误。什么样的程序才是正确的？“测试测试”或或“调试调试”方法方法 采用“测试”方法可以发现程序中的错误，但却不能证明程序中没有错误！因此，为保证程序的正确性，必须从理论上研究有关“程序正确性证明”的方法。7/14/2024西南石油大学计算机科学学院西南石油大学计算机科学学院西南石油大学计算机科学学院西南石油大学计算机科学学院4程序正确性证明发展历程20世纪50年代 Turing开始研究1967年，Floyd和Naur提出不变式断言法1969年，Hoare提出公理化方法1975年，Dijkstra提出最弱前置谓词和程序推导方法，解决了断言构造难的问题，可从程序规约推导出正确程序，使正确性证明变得实用。程序正确性理论是十分活跃的课题，不仅可程序正确性理论是十分活跃的课题，不仅可以证明顺序程序的正确性，而且还可以证明非确以证明顺序程序的正确性，而且还可以证明非确定性程序，以及并行程序的正确性。定性程序，以及并行程序的正确性。7/14/2024西南石油大学计算机科学学院西南石油大学计算机科学学院西南石油大学计算机科学学院西南石油大学计算机科学学院5程序正确性理论 程序设计的一般过程 7/14/2024西南石油大学计算机科学学院西南石油大学计算机科学学院西南石油大学计算机科学学院西南石油大学计算机科学学院6程序正确性理论 程序功能的精确描述 1、程序规约：对程序所实现功能的精确描述，由程序的前置断言和后置断言两部分组成。2、前置断言：程序执行前的输入应满足的条件，又称为输入断言。3、后置断言：程序执行后的输出应满足的条件，又称为输出断言。程序设计过程：问题 程序规约 程序7/14/2024西南石油大学计算机科学学院西南石油大学计算机科学学院西南石油大学计算机科学学院西南石油大学计算机科学学院7程序规约的基本分类非形式化程序规约 非形式化程序规约采用自然语言描述程序功能，简单、方便，但存在二义性，因此，不利于程序的正确性证明。形式化程序规约 采用数学化的语言描述程序功能，描述精确，无二义性，便于程序的正确性证明。7/14/2024西南石油大学计算机科学学院西南石油大学计算机科学学院西南石油大学计算机科学学院西南石油大学计算机科学学院8程序规约的实例（1/2）在书写程序规约时，使用Q表示前置断言，R表示后置断言，S表示问题求解的实现程序。在前置断言Q之前，还必须给出Q和R中所出现的标识符的必要说明。例1：求数组b0:n-1中所有元素的最大值。in n:integer;in b0:n-1:array of integer;out y:integer Q:n 1 S R:y MAX（i:0 i n;bi)7/14/2024西南石油大学计算机科学学院西南石油大学计算机科学学院西南石油大学计算机科学学院西南石油大学计算机科学学院9例2：求两个非负整数的最大公约数。in a,b:integer;out y:integer Q:a 0 b 0 S R:y MAX（i:1 i min(a,b)(a mod i 0)(b mod i 0);i)程序规约的实例（2/2）7/14/2024西南石油大学计算机科学学院西南石油大学计算机科学学院西南石油大学计算机科学学院西南石油大学计算机科学学院10程序正确性定义（1/3）衡量一个程序的正确性，主要看程序是否实现了问题所要求的功能。若程序实现了问题所要求的功能，则称它为正确的，否则是不正确的。程序设计过程：问题 程序规约 程序 对程序的正确性理解，可以分为两个层次：从广义来说，一个程序的正确性取决于该程序满足问题实际需求的程度。从狭义而言，如果一个程序满足了它的程序规约就是正确的。7/14/2024西南石油大学计算机科学学院西南石油大学计算机科学学院西南石油大学计算机科学学院西南石油大学计算机科学学院11uu程序规约程序规约QSR QSR 是一个逻辑表达式，其取值为真或假，其是一个逻辑表达式，其取值为真或假，其中取值为真的含义是指：给定一段程序中取值为真的含义是指：给定一段程序S S，若程序开始执行，若程序开始执行之前之前Q Q为真，为真，S S的执行将终止，且终止时的执行将终止，且终止时R R为真，则称为为真，则称为“程程序序S S，关于前置断言，关于前置断言Q Q和后置断言和后置断言R R是完全正确的是完全正确的”。程序正确性定义（2/3）7/14/2024西南石油大学计算机科学学院西南石油大学计算机科学学院西南石油大学计算机科学学院西南石油大学计算机科学学院12uu部分正确部分正确部分正确部分正确：若对于每个使得：若对于每个使得Q(i)Q(i)为真，并且程序为真，并且程序S S计算终止的计算终止的输入信息输入信息i i，R(i,S(i)R(i,S(i)都为真，则称程序都为真，则称程序S S关于关于Q Q和和R R是部分正是部分正确的。确的。uu程序终止程序终止程序终止程序终止：若对于每个使得：若对于每个使得Q(i)Q(i)为真的输入为真的输入i i，程序，程序S S的计算的计算都终止，则称程序都终止，则称程序S S关于关于Q Q是终止的。是终止的。uu完全正确完全正确完全正确完全正确：程序是部分正确，同时又是终止的。：程序是部分正确，同时又是终止的。程序正确性定义（3/3）7/14/2024西南石油大学计算机科学学院西南石油大学计算机科学学院西南石油大学计算机科学学院西南石油大学计算机科学学院13uu（1 1）证明部分正确性的方法）证明部分正确性的方法 A.Floyd A.Floyd的不变式断言法的不变式断言法 B.Manna B.Manna的子目标断言法的子目标断言法uu C.Hoare C.Hoare的公理化方法的公理化方法uu（2 2）终止性证明的方法）终止性证明的方法uu A.Floyd A.Floyd的良序集方法的良序集方法uu B.Knuth B.Knuth的计数器方法的计数器方法uu C.Manna C.Manna等人的不动点方法等人的不动点方法uu（3 3）完全正确性的方法）完全正确性的方法uu A.Hoare A.Hoare公理化方法的推广公理化方法的推广uu B.Burstall B.Burstall的间发断言法的间发断言法uu C.Dijkstra C.Dijkstra的弱谓词变换方法以及强验证方法的弱谓词变换方法以及强验证方法程序正确性的证明方法分类程序正确性的证明方法分类程序正确性的证明方法分类程序正确性的证明方法分类7/14/2024西南石油大学计算机科学学院西南石油大学计算机科学学院西南石油大学计算机科学学院西南石油大学计算机科学学院14循环不变式断言把反映循环变量的变化规律，且在每次循环体的执行前后均为真的逻辑表达式称为该循环的不变式断不变式断言言。例 带余整数除法问题：设x为非负整数，y为正整数，求x除以y的商q，以及余数r。程序：q0；rx；while(r y)/该循环不变式断言：/(xyqr)r 0 r ry；q q1；7/14/2024西南石油大学计算机科学学院西南石油大学计算机科学学院西南石油大学计算机科学学院西南石油大学计算机科学学院15不变式断言法不变式断言法不变式断言法不变式断言法uu证明步骤：证明步骤：1 1、建立断言：建立程序的输入、输出断言，如果程序、建立断言：建立程序的输入、输出断言，如果程序、建立断言：建立程序的输入、输出断言，如果程序、建立断言：建立程序的输入、输出断言，如果程序中有循环出现的话，在循环中选取一个断点，在断点中有循环出现的话，在循环中选取一个断点，在断点中有循环出现的话，在循环中选取一个断点，在断点中有循环出现的话，在循环中选取一个断点，在断点处建立一个循环不变式断言处建立一个循环不变式断言处建立一个循环不变式断言处建立一个循环不变式断言2 2、建立检验条件，将程序分解为不同的通路，为每一、建立检验条件，将程序分解为不同的通路，为每一、建立检验条件，将程序分解为不同的通路，为每一、建立检验条件，将程序分解为不同的通路，为每一个通路建立一个检验条件，该检验条件为如下形式：个通路建立一个检验条件，该检验条件为如下形式：个通路建立一个检验条件，该检验条件为如下形式：个通路建立一个检验条件，该检验条件为如下形式：I I R=O,R=O,其中其中其中其中I I为输入断言，为输入断言，为输入断言，为输入断言，R R为进入通路的条件，为进入通路的条件，为进入通路的条件，为进入通路的条件，OO为输出断言为输出断言为输出断言为输出断言3 3、证明检验条件：运用数学工具证明步骤、证明检验条件：运用数学工具证明步骤、证明检验条件：运用数学工具证明步骤、证明检验条件：运用数学工具证明步骤2 2得到的所得到的所得到的所得到的所有检验条件，如果每一条通路检验条件都为真，则该有检验条件，如果每一条通路检验条件都为真，则该有检验条件，如果每一条通路检验条件都为真，则该有检验条件，如果每一条通路检验条件都为真，则该程序为部分正确的。程序为部分正确的。程序为部分正确的。程序为部分正确的。7/14/2024西南石油大学计算机科学学院西南石油大学计算机科学学院西南石油大学计算机科学学院西南石油大学计算机科学学院16不变式断言法实例不变式断言法实例不变式断言法实例不变式断言法实例1 1uu例：设例：设x,yx,y为正整数，求为正整数，求x,yx,y的最大公约数的最大公约数z z的程序，即的程序，即z=gcd(x,y)z=gcd(x,y)。若y1y2，gcd(y1,y2)=gcd(y1-y2,y2)若y2y1，gcd(y1,y2)=gcd(y1,y2-y1)若y1=y2，gcd(y1,y2)=y1=y27/14/2024西南石油大学计算机科学学院西南石油大学计算机科学学院西南石油大学计算机科学学院西南石油大学计算机科学学院17不变式断言法实例不变式断言法实例不变式断言法实例不变式断言法实例1 1uu例：设例：设x,yx,y为正整数，求为正整数，求x,yx,y的最大公约数的最大公约数z z的程序，即的程序，即z=gcd(x,y)z=gcd(x,y)。Function gcd(x1,x2:integer);var y1,y2,z:Integer;Beginy1:=x1;y2:=x1;while y1y2 do if y1y2 then y1:=y1-y2 else y2:=y2-y1 end;z:=y1;write(z);End.START(x1,x2)-(y1,y2)y1y2y1y2y1:=y1-y2y2:=y2-y1z:=y1STOPTFTF7/14/2024西南石油大学计算机科学学院西南石油大学计算机科学学院西南石油大学计算机科学学院西南石油大学计算机科学学院18不变式断言法实例不变式断言法实例不变式断言法实例不变式断言法实例1 1(建立断言建立断言建立断言建立断言)uu输入断言：输入断言：输入断言：输入断言：I(x1,x2):x10I(x1,x2):x10I(x1,x2):x10I(x1,x2):x10 x20 x20 x20 x20uu输出断言：输出断言：输出断言：输出断言：O(x1,x2,z):z=gcd(x1,x2)O(x1,x2,z):z=gcd(x1,x2)O(x1,x2,z):z=gcd(x1,x2)O(x1,x2,z):z=gcd(x1,x2)uu循环不变式断言循环不变式断言循环不变式断言循环不变式断言(断点选为断点选为断点选为断点选为b):b):b):b):P(x1,x2,y1,y2):x10 P(x1,x2,y1,y2):x10 P(x1,x2,y1,y2):x10 P(x1,x2,y1,y2):x10 x20 x20 x20 x20 y10 y10 y10 y10 y20 y20 y20 y20 gcd(y1,y2)=gcd(x1,x2)gcd(y1,y2)=gcd(x1,x2)gcd(y1,y2)=gcd(x1,x2)gcd(y1,y2)=gcd(x1,x2)通路划分：通路划分：通路通路1：a-b通路通路2：b-d-b通路通路3：b-e-b通路通路4：b-g-cO(x,y,z)START(x1,x2)-(y1,y2)y1y2y1y2y1:=y1-y2y2:=y2-y1z:=y1STOPTFTFI(x1,x2)aP(x1,x2,y1,y2)bcdeg7/14/2024西南石油大学计算机科学学院西南石油大学计算机科学学院西南石油大学计算机科学学院西南石油大学计算机科学学院19不变式断言法实例不变式断言法实例不变式断言法实例不变式断言法实例1 1(建立检验条件建立检验条件建立检验条件建立检验条件)uu检验条件：检验条件：I I R=O R=Ouu通路通路1 1：I(x1,x2)=P(x1,x2,y1,y2)(I(x1,x2)=P(x1,x2,y1,y2)(无条件无条件)x10 x10 x20 x20 x10 x10 x20 x20 y10 y10 y20 y20 gcd(y1,y2)=gcd(x1,x2)gcd(y1,y2)=gcd(x1,x2)uu通路通路2 2：P(x1,x2,y1,y2)P(x1,x2,y1,y2)y1y2 y1y2 y1y2=P(x1,x2,y1-y2,y2)y1y2=P(x1,x2,y1-y2,y2)x10 x10 x20 x20 y10 y10 y20 y20 gcd(y1,y2)=gcd(x1,x2)gcd(y1,y2)=gcd(x1,x2)y1y2 y1y2 y1y2 y1y2=x10 x10 x20 x20 y1-y20 y1-y20 y20 y20 gcd(y1-y2,y2)=gcd(x1,x2)gcd(y1-y2,y2)=gcd(x1,x2)uu通路通路3 3：P(x1,x2,y1,y2)P(x1,x2,y1,y2)y1y2 y1y2 y1 P(x1,x2,y1,y2-y1)y1 P(x1,x2,y1,y2-y1)uu通路通路4 4：P(x1,x2,y1,y2)P(x1,x2,y1,y2)y1=y2=O(x1,x2,z)y1=y2=O(x1,x2,z)7/14/2024西南石油大学计算机科学学院西南石油大学计算机科学学院西南石油大学计算机科学学院西南石油大学计算机科学学院20不变式断言法实例不变式断言法实例不变式断言法实例不变式断言法实例1 1(证明检验条件证明检验条件证明检验条件证明检验条件)uu通路通路1 1：无需证明：无需证明uu通路通路2 2：前提：前提：前提：前提：P(x1,x2,y1,y2)P(x1,x2,y1,y2)y1y2 y1y2 y1y2=P(x1,x2,y1-y2,y2)y1y2=P(x1,x2,y1-y2,y2)即：即：x10 x10 x20 x20 y10 y10 y20 y20 gcd(y1,y2)=gcd(x1,x2)gcd(y1,y2)=gcd(x1,x2)y1y2 y1y2 y1y2 y1y2 结论结论：x10 x10 x20 x20 y1-y20 y1-y20 y20 y20 gcd(y1-y2,y2)=gcd(x1,x2)gcd(y1-y2,y2)=gcd(x1,x2)证明：因为证明：因为y1y2,y1y2,所以所以y1-y20y1-y20成立成立,因此有因此有 gcd(y1-y2,y2)=gcd(y1,y2)=gcd(x1,x2)gcd(y1-y2,y2)=gcd(y1,y2)=gcd(x1,x2)得得证证uu通路通路3:y2y13:y2y1则则gcd(y1,y2-y1)=gcd(y1,y2)=gcd(x1,x2)gcd(y1,y2-y1)=gcd(y1,y2)=gcd(x1,x2)uu通路通路4:z=y1=y24:z=y1=y2则则gcd(y1,y2)=y1=y2,gcd(y1,y2)=y1=y2,又因又因gcd(x1,x2)=gcd(y1,y2)gcd(x1,x2)=gcd(y1,y2)成立，成立，所以所以 Z=gcd(x1,x2)Z=gcd(x1,x2)成立成立 7/14/2024西南石油大学计算机科学学院西南石油大学计算机科学学院西南石油大学计算机科学学院西南石油大学计算机科学学院21不变式断言法实例不变式断言法实例不变式断言法实例不变式断言法实例2 2uu对任一给定的自然数对任一给定的自然数x x，计算，计算z z ，即计算，即计算x x的平方根的平方根取整取整uu1 13 3(2n+1)=(n+1)(2n+1)=(n+1)2 2(定定理理)设设y1=n;y1=n;y3=2y1+1 y3=2y1+1；y2=(y1+1)y2=(y1+1)2 2;uu输入断言：输入断言：I(x):x0 I(x):x0uu输出断言：输出断言：O(x,z):z O(x,z):z2 2 x(z+1)x(z+1)2 2uu循环不变式：循环不变式：P(x,y1,y2,y3)P(x,y1,y2,y3)：y1 y12 2 x(y1,y2,y3)y2+y3-y2y2x(y1+1,y3+2)-(y1,y3)y1-z结束A I(x)B P(x,y1,y2,y3)DC O(x,z)TF7/14/2024西南石油大学计算机科学学院西南石油大学计算机科学学院西南石油大学计算机科学学院西南石油大学计算机科学学院22不变式断言法实例不变式断言法实例不变式断言法实例不变式断言法实例uu建立检验条件：建立检验条件：uu通路通路1 1：A-BA-BI(x)=P(x,0,1,1)I(x)=P(x,0,1,1)I(x)=P(x,0,1,1)I(x)=P(x,0,1,1)x0=0 0=0 0=0 0=0 D-BB-D-BP(x,y1,y2,y3)P(x,y1,y2,y3)P(x,y1,y2,y3)P(x,y1,y2,y3)y2 p(x,y1+1,y2+y3+2,y3+2)y2 p(x,y1+1,y2+y3+2,y3+2)y2 p(x,y1+1,y2+y3+2,y3+2)y2 p(x,y1+1,y2+y3+2,y3+2)y1 y12 2x x y2=(y1+1)y2=(y1+1)2 2 y3=2y1+1 y3=2y1+1 y2 y2 (y1+1)(y1+1)2 2 x CB-CP(x,y1,y2,y3)P(x,y1,y2,y3)P(x,y1,y2,y3)P(x,y1,y2,y3)y2x=O(x,y)y2x=O(x,y)y2x=O(x,y)y2x=O(x,y)y1y1y1y12 2 2 2x x x x=y1 y2x=y1 y2x=y1 y2x=y12 2 2 2x(y1+1)x(y1+1)x(y1+1)x(y1+1)2 2 2 27/14/2024西南石油大学计算机科学学院西南石油大学计算机科学学院西南石油大学计算机科学学院西南石油大学计算机科学学院23不变式断言法实例不变式断言法实例不变式断言法实例不变式断言法实例uu检验条件检验条件2 2uuy1y12 2 x x=uu (y1+1)(y1+1)2 2 x x y2+y3+2=(y1+1+1)y2+y3+2=(y1+1+1)2 2 y3+1=2(y1+1)+1 y3+1=2(y1+1)+1uu证明：证明：uu x(y1+1)x(y1+1)2 2y2+y3+2=(y1+1)y2+y3+2=(y1+1)2 2+2y1+1+2=(y1+2)+2y1+1+2=(y1+2)2 2y3+2=2y1+1+2=2(y1+1)+1y3+2=2y1+1+2=2(y1+1)+1uu检验条件检验条件3 3y1y12 2 x x=y2x=y1y12 2 x(y1+1)x(y1+1)2 2uu 证明：证明：uu y1 y12 2 xxuu xy2,y2=(y1+1)xxx0 I(x,y):x00 y00 y00uu输出断言：输出断言：O(x,y,z):z=gcd(x,y)O(x,y,z):z=gcd(x,y)uu循环不变式断言：循环不变式断言：P(x,y):x=0 P(x,y):x=0 y=0 y=0 gcd(x,y)=gcd(x0,y0)gcd(x,y)=gcd(x0,y0)STARTRead(x,y)x0yxy:=y-xx yz:=ySTOPTFTFI(x,y)aP(x,y)bcO(x,y,z)deg例：设x,y为正整数，求x,y的最大公约数z的程序，即z=gcd(x,y)。7/14/2024西南石油大学计算机科学学院西南石油大学计算机科学学院西南石油大学计算机科学学院西南石油大学计算机科学学院26子目标断言法子目标断言法子目标断言法子目标断言法(建立断言建立断言建立断言建立断言)uu输入断言输入断言I(x,y):x00 I(x,y):x00 y00 y00uu输出断言输出断言O(x,y,z):z=gcd(x,y)O(x,y,z):z=gcd(x,y)uu子目标断言子目标断言(b(b为循环断为循环断点点)P(x,y,yP(x,y,yendend):x=0):x=0 y=0 y=0=y=yendend=gcd(x,y)=gcd(x,y)含义：每当控制以含义：每当控制以x x和和y y的的容许值通过容许值通过b b时，时，x x和和y y的当前值的最大公约数的当前值的最大公约数将等于将等于y y的最终值的最终值STARTRead(x,y)x0yxy:=y-xx yz:=ySTOPTFTFI(x,y)aP(x,y)bcO(x,y,z)deg7/14/2024西南石油大学计算机科学学院西南石油大学计算机科学学院西南石油大学计算机科学学院西南石油大学计算机科学学院27子目标断言法子目标断言法子目标断言法子目标断言法(建立检验条件建立检验条件建立检验条件建立检验条件)uu通路通路1 1：b-c b-c 检验条件检验条件1 1x=0=x=0 x=0=x=0 y=0 y=0=y yendend=gcd(x,y)=gcd(x,y)uu通路通路2 2：b-d-b b-d-b 检验条件检验条件2 2P(x,y-x,yP(x,y-x,yendend)x0 x0 yx=P(x,y,y yx=P(x,y,yendend)x=0 x=0 y-x=0 y-x=0 y yendend=gcd(x,y-x)=gcd(x,y-x)x0 x0 y=x=y=x=x=0 x=0 y=0 y=0 y yendend=gcd(x,y)=gcd(x,y)uu通路通路3 3：b-e-b b-e-b 检验条件检验条件3 3P(y,x,yP(y,x,yendend)x0 x0 y P(x,y,y y P(x,y,yendend)uu通路通路4 4：a-b a-b 检验条件检验条件4 4x00 x00 y00 y00 P(x0,y0,y P(x0,y0,yendend)=y)=yendend=gcd(x0,y0)=gcd(x0,y0)7/14/2024西南石油大学计算机科学学院西南石油大学计算机科学学院西南石油大学计算机科学学院西南石油大学计算机科学学院28子目标断言法子目标断言法子目标断言法子目标断言法(证明检验条件证明检验条件证明检验条件证明检验条件)uu检验条件检验条件1 1：x=0=x=0 x=0=x=0 y=0 y=0 =y yendend=gcd(x,y)=gcd(x,y)证明：证明：因为有因为有 x=0,y x=0,yendend=y=y所以所以 y yendend=y=gcd(0,y)=y=gcd(0,y)=gcd(x,y)=gcd(x,y)uu检验条件检验条件2 2：P(x,y-x,yP(x,y-x,yendend)x0 x0 yx=P(x,y,y yx=P(x,y,yendend)即证明：即证明：x=0 x=0 y-x=0 y-x=0 y yendend=gcd(x,y-x)=gcd(x,y-x)x0 x0 y=x=y=x=x=0 x=0 y=0 y=0 y yendend=gcd(x,y)=gcd(x,y)由：由：x0 x0 y=x =y0,y=x =y0,以及以及 gcd(x,y-x)=gcd(x,y)gcd(x,y-x)=gcd(x,y)，可知，可知 y yendend gcd(x,y-x)gcd(x,y-x)gcd(x,y)gcd(x,y)7/14/2024西南石油大学计算机科学学院西南石油大学计算机科学学院西南石油大学计算机科学学院西南石油大学计算机科学学院29uu终止性证明的方法终止性证明的方法FloydFloyd的良序集方法的良序集方法的良序集方法的良序集方法KnuthKnuth的计数器方法的计数器方法的计数器方法的计数器方法7/14/2024西南石油大学计算机科学学院西南石油大学计算机科学学院西南石油大学计算机科学学院西南石油大学计算机科学学院30程序部分正确但不终止实例Program A var x,y,z,s:integer;begin read(x,y);while x 0 do if y=x then y=y x;else x=x y;z=y;write(z);end.STARTRead(x,y)x0y=xy:=y-xx:=x-yz:=ySTOPTFTFI(x,y)aP(x,y)bcO(x,y,z)deg例：求两个正整数x、y的最大公约数z的程序。可以利用不变式断言证明该程序的部分正确性，但无法证明它是终止的。因为当y0时，程序循环将不终止！7/14/2024西南石油大学计算机科学学院西南石油大学计算机科学学院西南石油大学计算机科学学院西南石油大学计算机科学学院31本课的内容本课的内容本课的内容本课的内容uu程序终止性证明方法：良序集方法程序终止性证明方法：良序集方法uu程序终止性证明方法：计数器方法程序终止性证明方法：计数器方法7/14/2024西南石油大学计算机科学学院西南石油大学计算机科学学院西南石油大学计算机科学学院西南石油大学计算机科学学院32良序集方法证明程序终止性良序集方法证明程序终止性良序集方法证明程序终止性良序集方法证明程序终止性uu1.1.基本概念基本概念偏序集偏序集偏序集偏序集良序集良序集良序集良序集uu2.2.采用良序集方法证明程序终止性采用良序集方法证明程序终止性7/14/2024西南石油大学计算机科学学院西南石油大学计算机科学学院西南石油大学计算机科学学院西南石油大学计算机科学学院33良序集的概念（良序集的概念（良序集的概念（良序集的概念（1/21/2）1.1.偏序集偏序集偏序集偏序集设有一个非空集合设有一个非空集合WW和一个定义在和一个定义在WW上的二元关系上的二元关系 ，且这个关系，且这个关系 满足下满足下列性质：列性质：1 1）传递性，即对于一切）传递性，即对于一切a,b,ca,b,cW,W,如果如果ab,bc ab,bc，则，则acac2 2）反对称性，即对于）反对称性，即对于aab,b,则有则有b baa3 3）反自反性，即对于一切）反自反性，即对于一切aWaW，a a aa称称W W为具有关系为具有关系 的偏序集，记做（的偏序集，记做（W,W,）例如：例如：（1 1）具有小于关系（）具有小于关系（）的，位于）的，位于0 01 1之间的实数集合之间的实数集合A1A1。（2 2）具有小于关系（）具有小于关系（）的全体整数集合）的全体整数集合B1B1。但将但将 换成换成 就不是就不是偏序集。偏序集。（1 1）具有小于关系（）具有小于关系（）的，位于）的，位于0 01 1之间的实数集合之间的实数集合A1A1。（2 2）具有小于关系（）具有小于关系（）的全体整数集合）的全体整数集合B1B1。7/14/2024西南石油大学计算机科学学院西南石油大学计算机科学学院西南石油大学计算机科学学院西南石油大学计算机科学学院34良序集的概念（2/2）2.2.良序集良序集设（W,）是偏序集，如果不存在由W中的元素构成的无限递减序列:a2a1a0，则称（W,）是良序集。例如：（1）若N是自然数集合，那么（N，）是良序集。（2）具有通常序A B C Z的字母表=A,B,Z是良序集。但下述集合A1和B1是偏序集，但不是良序集。（1）具有小于关系（）的，位于01之间的实数集合A1。（2）具有小于关系（）的全体整数集合B1。7/14/2024西南石油大学计算机科学学院西南石油大学计算机科学学院西南石油大学计算机科学学院西南石油大学计算机科学学院35采用良序集证明程序终止性思路1 1、结构化程序由顺序、选择和循环三种基本结构组、结构化程序由顺序、选择和循环三种基本结构组成，而影响程序终止性的是循环结构，因此，是程序成，而影响程序终止性的是循环结构，因此，是程序终止性证明的重点。终止性证明的重点。2 2、程序终止性证明思路：、程序终止性证明思路：A.A.选取良序集合（选取良序集合（W,W,）；）；B.B.选取割点集，割断循环；选取割点集，割断循环；C.C.在割点上寻找函数在割点上寻找函数u,u,使使uWuW；D.D.证明每次循环，证明每次循环，u u依次递减。依次递减。由于良序集合（由于良序集合（W,W,）不存在无穷递减序列，因此，）不存在无穷递减序列，因此，循环必然终止。循环必然终止。7/14/2024西南石油大学计算机科学学院西南石油大学计算机科学学院西南石油大学计算机科学学院西南石油大学计算机科学学院36用良序集方法证明程序终止性步骤用良序集方法证明程序终止性步骤用良序集方法证明程序终止性步骤用良序集方法证明程序终止性步骤uu1.1.选取一个点集去截断程序的各个循环部分，并在每个截断选取一个点集去截断程序的各个循环部分，并在每个截断点点I I处建立中间断言处建立中间断言Q Qi i(x,y)(x,y)uu2.2.选取一个良序集选取一个良序集(W,)(W,Q(x,y)=Qj j(x,r(x,raj aj(x,y)(x,y)证明对每一个从截断点证明对每一个从截断点i i到截断点到截断点j j的通路的通路aijaij，有，有 Q Qi i(x,y)(x,y)R R a i ja i j(x,y)=Q (x,y)=Q j j(x,r (x,r a i ja i j(x,y)(x,y)即证明中间断言是即证明中间断言是“正确的正确的”，是，是“良断言良断言”uu4.4.证明证明 Q Qi i(x,y)=E(x,y)=E i i(x,y)(x,y)W W，即终止表达式是良函数，即终止表达式是良函数uu5.5.证明对于每一个从截断点证明对于每一个从截断点i i到截断点到截断点j j的通路的通路aijaij，有，有 Q Qi i(x,y)(x,y)R Raj aj(x,y)=E(x,y)=E j j (x,y)E(x,y)(y1,y2,y3)y2+y3-y2y2 x(y1+1,y3+2)-(y1,y3)y1-z结束BTF7/14/2024西南石油大学计算机科学学院西南石油大学计算机科学学院西南石油大学计算机科学学院西南石油大学计算机科学学院38良序集方法证明程序终止性实例良序集方法证明程序终止性实例良序集方法证明程序终止性实例良序集方法证明程序终止性实例uu1.1.选取断点选取断点B B，建立中间断言，建立中间断言 Q(x,y1,y2,y3):y2 x Q(x,y1,y2,y3):y2 0 y30uu2.2.取良序集（取良序集（N,N,B-B：I(x)=Q(x,y1,y2,y3)I(x)=Q(x,y1,y2,y3)，即：即：x0=00=00 10 从截断点从截断点B-BB-B：Q(x,y1,y2,y3)Q(x,y1,y2,y3)y2+y3 Q(x,y1+1,y2+y3,y3+2)y2+y3 Q(x,y1+1,y2+y3,y3+2)即：即：y2x y20 y30 y2+y3 y2+y3x y2+y3 y2+y30 y3+207/14/2024西南石油大学计算机科学学院西南石油大学计算机科学学院西南石油大学计算机科学学院西南石油大学计算机科学学院39良序集方法证明程序终止性实例良序集方法证明程序终止性实例良序集方法证明程序终止性实例良序集方法证明程序终止性实例uu4.4.证明证明E(x,y)E(x,y)是良函数，即证明是良函数，即证明q(x,y)=E(x,y)q(x,y)=E(x,y)N N，即，即 y2x y20=x-y20 y30=x-y20 所以所以x-y2x-y2 N Nuu5.5.证明终止条件成立证明终止条件成立 Q(x,y)Q(x,y)y2+y3 E(x,y1+1,y2+y3,y3+2)E(x,y1,y2,y3)y2+y3 E(x,y1+1,y2+y3,y3+2)E(x,y1,y2,y3)即：即：y2x y20 y30 y2+y3 x-y2-y3 x-y2 y2+y3 x-y2-y3 x-y27/14/2024西南石油大学计算机科学学院西南石油大学计算机科学学院西南石油大学计算机科学学院西南石油大学计算机科学学院40采用良序集证明程序终止性总结1 1、采用良序集方法证明程序终止性，关键在于选择、采用良序集方法证明程序终止性，关键在于选择合适的良序集合适的良序集Q Qi i(x,y)(x,y)和终止表达式和终止表达式E Ei i(x,y)(x,y)。2 2、采用良序集证明程序终止性，与程序部分正确性、采用良序集证明程序终止性，与程序部分正确性证明采用了不同途径，相互完全独立，因此，证明程证明采用了不同途径，相互完全独立，因此，证明程序的完全正确性工作量较大。序的完全正确性工作量较大。3 3、采用计数器方法可以将程序的部分正确性和终止、采用计数器方法可以将程序的部分正确性和终止性证明结合进行。性证明结合进行。7/14/2024西南石油大学计算机科学学院西南石油大学计算机科学学院西南石油大学计算机科学学院西南石油大学计算机科学学院41计数器方法证明程序终止性证明思路通过估计循环执行的最大次数的方法。证明步骤1.为程序的每一个循环附加一个新的变量作为该循环的计数器，初始值置为0，每循环一次该计数器加1。2.为每个循环设置一个中间断言，它表示相应的计数器不会超过固定的界限。3.证明（2）中的中间断言是不变式断言。7/14/2024西南石油大学计算机科学学院西南石油大学计算机科学学院西南石油大学计算机科学学院西南石油大学计算机科学学院42计数器方法证明程序终止性实例计数器方法证明程序终止性实例计数器方法证明程序终止性实例计数器方法证明程序终止性实例uu计算非负整数的计算非负整数的最大公约数最大公约数STARTRead(x,y)x0y xy:=y-xx yz:=ySTOPTFTFI(x,y)aP(x,y)bdevar x,y,z,s:integer;begin Read(x,y)while x0 do begin If yx then y:=y-x;else s:=x;x:=y;y:=s;endz:=y;write(z);end.7/14/2024西南石油大学计算机科学学院西南石油大学计算机科学学院西南石油大学计算机科学学院西南石油大学计算机科学学院43计数器方法证明程序终止性实例计数器方法证明程序终止性实例计数器方法证明程序终止性实例计数器方法证明程序终止性实例uu1.1.引进计数器引进计数器I,I,并建立如下断言并建立如下断言 x=0 y=0 2x+y+I x=0 y=0 2x+y+I 2x0+y0 2x0+y0var x,y,z,s:integer;var x,y,z,s:integer;read(x,y);read(x,y);I:=0;/I:=0;/计数器赋初值计数器赋初值while x0 dowhile x0 dobeginbegin If yx then y:=y-x;If yx then y:=y-x;else s:=x;x:=y;y:=s;else s:=x;x:=y;y:=s;I:=I+1;/I:=I+1;/计数器递增计数器递增计数器递增计数器递增endendz:=y;z:=y;write(z);write(z);7/14/2024西南石油大学计算机科学学院西南石油大学计算机科学学院西南石油大学计算机科学学院西南石油大学计算机科学学院44计数器方法证明程序终止性实例计数器方法证明程序终止性实例计数器方法证明程序终止性实例计数器方法证明程序终止性实例2.2.建立检验条件并证明，从而证明计数器断言为不变式断言建立检验条件并证明，从而证明计数器断言为不变式断言检验条件检验条件1 1：a-ba-bx0=0 y0=0 =x0=0 y0=0 2x0+y0+0 x0=0 y0=0 =x0=0 y0=0 2x0+y0+0 2x0+y0 2x0+y0检验条件检验条件2 2：b-d-bb-d-bx=0 y=0 (2x+y+I x=0 y=0 (2x+y+I 2x0+y0)x0 y=x=2x0+y0)x0 y=x=x=0 y-x=0 (2x+(y-x)+I+1)x=0 y-x=0 (2x+(y-x)+I+1)2x0+y0)2x0+y0)证明：证明：(x-1=0)(x-1=0)2x+(y-x)+I+1=2x+y+I-(x-1)=2x+y+I 2x+(y-x)+I+1=2x+y+I-(x-1)e-bb-e-bx=0 y=0 (2x+y+I x=0 y=0 (2x+y+I 2x0+y0)x0 y 2x0+y0)x0 yy=0 x=0 2y+x+I+1 y=0 x=0 2y+x+I+1 2x0+y0 2x0+y0 证明：证明：(yx x0 x1=yx-1)(yx x0 x1=yx-1)2y+x+I+1 y+2x+I 2x0+y0 2y+x+I+1 y+2x+I 0N(x,y)0。1.2 1.2 每次循环，每次循环，N(x,y)N(x,y)都减小。都减小。由由N(x,y)N(x,y)的值构成一个单调递减的整数序列，的值构成一个单调递减的整数序列，N(x,y)0 N(x,y)0，因而，因而，循环只能执行有限次。循环只能执行有限次。7/14/2024西南石油大学计算机科学学院西南石油大学计算机科学学院西南石油大学计算机科学学院西南石油大学计算机科学学院46另一种计数器方法证明程序终止性实例另一种计数器方法证明程序终止性实例另一种计数器方法证明程序终止性实例另一种计数器方法证明程序终止性实例uu例：例：设设x,yx,y为正整数，求为正整数，求x,yx,y的最大公约数的最大公约数z z的程的程序，即序，即z=gcd(x,y)z=gcd(x,y)。uu选取选取 N(y1,y2)=max(y1,y2)N(y1,y2)=max(y1,y2)uu容易证明：容易证明：uuN(y1,y2)0;N(y1,y2)0;uuN(y1,y2)N(y1,y2)是递减的。是递减的。START(x1,x2)-(y1,y2)y1y2y1y2y1:=y1-y2y2:=y2-y1z:=y1STOPTFTF7/14/2024西南石油大学计算机科学学院西南石油大学计算机科学学院西南石油大学计算机科学学院西南石油大学计算机科学学院47采用计数器方法证明程序终止性难点 采用计数器方法证明程序终止性关键在于确定一个合适的中间断言（或选取一个合适的函数N（x,y），尤其对于一些循环次数事先难以估计的程序，要找出循环次数的上限更为困难。7/14/2024西南石油大学计算机科学学院西南石油大学计算机科学学院西南石油大学计算机科学学院西南石油大学计算机科学学院48作业作业作业作业START(0，1)-(sum，I)I(sum，I)Z=sumSTOPTF1 1。下图是计算。下图是计算sum=Xsum=Xi i的流程图程序，试证明它的部分正确的流程图程序，试证明它的部分正确性和终止性性和终止性为方便学习与回顾本课程，请在下载后进行查阅和编辑，疑问之处请直接联系老师Fortheconvenienceoflearningandreviewingthiscourse,pleasecheckandedititafterdownloading.Ifyouhaveanyquestions,pleasecontacttheteacherdirectly