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

西南石油大学计算机科学学院1第三章程序正确性证明西南石油大学计算机科学学院2•什么样的程序才是正确的？如何来保证程序是正确的？程序正确性概述西南石油大学计算机科学学院3关于程序正确性的认识根据问题的特性和软件所要实现的功能，选择一些具有代表性的数据，设计测试用例。通过用例程序执行，去发现被测试程序的错误。•什么样的程序才是正确的？“测试”或“调试”方法采用“测试”方法可以发现程序中的错误，但却不能证明程序中没有错误！因此，为保证程序的正确性，必须从理论上研究有关“程序正确性证明”的方法。西南石油大学计算机科学学院4程序正确性证明发展历程•20世纪50年代Turing开始研究•1967年，Floyd和Naur提出不变式断言法•1969年，Hoare提出公理化方法•1975年，Dijkstra提出最弱前置谓词和程序推导方法，解决了断言构造难的问题，可从程序规约推导出正确程序，使正确性证明变得实用。程序正确性理论是十分活跃的课题，不仅可以证明顺序程序的正确性，而且还可以证明非确定性程序，以及并行程序的正确性。西南石油大学计算机科学学院5程序正确性理论•程序设计的一般过程西南石油大学计算机科学学院6程序正确性理论•程序功能的精确描述1、程序规约：对程序所实现功能的精确描述，由程序的前置断言和后置断言两部分组成。2、前置断言：程序执行前的输入应满足的条件，又称为输入断言。3、后置断言：程序执行后的输出应满足的条件，又称为输出断言。程序设计过程：问题程序规约程序西南石油大学计算机科学学院7程序规约的基本分类•非形式化程序规约非形式化程序规约采用自然语言描述程序功能，简单、方便，但存在二义性，因此，不利于程序的正确性证明。•形式化程序规约采用数学化的语言描述程序功能，描述精确，无二义性，便于程序的正确性证明。西南石油大学计算机科学学院8程序规约的实例（1/2）•在书写程序规约时，使用Q表示前置断言，R表示后置断言，S表示问题求解的实现程序。在前置断言Q之前，还必须给出Q和R中所出现的标识符的必要说明。例1：求数组b[0:n-1]中所有元素的最大值。[inn:integer;inb[0:n-1]:arrayofinteger;outy:integer]Q:{n≥1}SR:{y＝MAX（i:0≤i＜n;b[i])}西南石油大学计算机科学学院9例2：求两个非负整数的最大公约数。[ina,b:integer;outy:integer]Q:{a≥0∧b≥0}SR:{y＝MAX（i:1≤i≤min(a,b)∧(amodi＝0)∧(bmodi＝0);i)}程序规约的实例（2/2）西南石油大学计算机科学学院10程序正确性定义（1/3）•衡量一个程序的正确性，主要看程序是否实现了问题所要求的功能。若程序实现了问题所要求的功能，则称它为正确的，否则是不正确的。程序设计过程：问题程序规约程序对程序的正确性理解，可以分为两个层次：•从广义来说，一个程序的正确性取决于该程序满足问题实际需求的程度。•从狭义而言，如果一个程序满足了它的程序规约就是正确的。西南石油大学计算机科学学院11程序规约Q{S}R是一个逻辑表达式，其取值为真或假，其中取值为真的含义是指：给定一段程序S，若程序开始执行之前Q为真，S的执行将终止，且终止时R为真，则称为“程序S，关于前置断言Q和后置断言R是完全正确的”。程序正确性定义（2/3）西南石油大学计算机科学学院12部分正确：若对于每个使得Q(i)为真，并且程序S计算终止的输入信息i，R(i,S(i))都为真，则称程序S关于Q和R是部分正确的。程序终止：若对于每个使得Q(i)为真的输入i，程序S的计算都终止，则称程序S关于Q是终止的。完全正确：程序是部分正确，同时又是终止的。程序正确性定义（3/3）西南石油大学计算机科学学院13（1）证明部分正确性的方法A.Floyd的不变式断言法B.Manna的子目标断言法C.Hoare的公理化方法（2）终止性证明的方法A.Floyd的良序集方法B.Knuth的计数器方法C.Manna等人的不动点方法（3）完全正确性的方法A.Hoare公理化方法的推广B.Burstall的间发断言法C.Dijkstra的弱谓词变换方法以及强验证方法程序正确性的证明方法分类西南石油大学计算机科学学院14循环不变式断言•把反映循环变量的变化规律，且在每次循环体的执行前后均为真的逻辑表达式称为该循环的不变式断言。•例带余整数除法问题：设x为非负整数，y为正整数，求x除以y的商q，以及余数r。程序：q＝0；r＝x；while(r≥y)//该循环不变式断言：{//(x＝y×q＋r)∧r≥0r＝r－y；q＝q＋1；}西南石油大学计算机科学学院15不变式断言法证明步骤：1、建立断言：建立程序的输入、输出断言，如果程序中有循环出现的话，在循环中选取一个断点，在断点处建立一个循环不变式断言2、建立检验条件，将程序分解为不同的通路，为每一个通路建立一个检验条件，该检验条件为如下形式：I∧R=O,其中I为输入断言，R为进入通路的条件，O为输出断言3、证明检验条件：运用数学工具证明步骤2得到的所有检验条件，如果每一条通路检验条件都为真，则该程序为部分正确的。西南石油大学计算机科学学院16不变式断言法实例1例：设x,y为正整数，求x,y的最大公约数z的程序，即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=y2西南石油大学计算机科学学院17不变式断言法实例1例：设x,y为正整数，求x,y的最大公约数z的程序，即z=gcd(x,y)。Functiongcd(x1,x2:integer);vary1,y2,z:Integer;Beginy1:=x1;y2:=x1;whiley1y2doify1y2theny1:=y1-y2elsey2:=y2-y1end;z:=y1;write(z);End.START(x1,x2)-(y1,y2)y1y2y1y2y1:=y1-y2y2:=y2-y1z:=y1STOPTFTF西南石油大学计算机科学学院18不变式断言法实例1(建立断言)输入断言：I(x1,x2):x10x20输出断言：O(x1,x2,z):z=gcd(x1,x2)循环不变式断言(断点选为b):P(x1,x2,y1,y2):x10x20y10y20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)bcdeg···西南石油大学计算机科学学院19不变式断言法实例1(建立检验条件)检验条件：I^R=O通路1：I(x1,x2)=P(x1,x2,y1,y2)(无条件)x10x20＝x10x20y10y20gcd(y1,y2)=gcd(x1,x2)通路2：P(x1,x2,y1,y2)y1y2y1y2=P(x1,x2,y1-y2,y2)x10x20y10y20gcd(y1,y2)=gcd(x1,x2)y1y2y1y2=x10x20y1-y20y20gcd(y1-y2,y2)=gcd(x1,x2)通路3：P(x1,x2,y1,y2)y1y2y1y2=P(x1,x2,y1,y2-y1)通路4：P(x1,x2,y1,y2)y1=y2=O(x1,x2,z)西南石油大学计算机科学学院20不变式断言法实例1(证明检验条件)通路1：无需证明通路2：前提：P(x1,x2,y1,y2)y1y2y1y2=P(x1,x2,y1-y2,y2)即：x10x20y10y20gcd(y1,y2)=gcd(x1,x2)y1y2y1y2结论：x10x20y1-y20y20gcd(y1-y2,y2)=gcd(x1,x2)证明：因为y1y2,所以y1-y20成立,因此有gcd(y1-y2,y2)=gcd(y1,y2)=gcd(x1,x2)得证通路3:y2y1则gcd(y1,y2-y1)=gcd(y1,y2)=gcd(x1,x2)通路4:z=y1=y2则gcd(y1,y2)=y1=y2,又因gcd(x1,x2)=gcd(y1,y2)成立，所以Z=gcd(x1,x2)成立西南石油大学计算机科学学院21不变式断言法实例2对任一给定的自然数x，计算z＝[]，即计算x的平方根取整1＋3＋…(2n+1)=(n+1)2(定理)设y1=n;y3=2×y1+1；y2=(y1+1)2;输入断言：I(x):x0输出断言：O(x,z):z2x(z+1)2循环不变式：P(x,y1,y2,y3)：y12xy2=(y1+1)2y3=2y1+1开始(0,0,1)-(y1,y2,y3)y2+y3-y2y2x(y1+1,y3+2)-(y1,y3)y1-z结束AI(x)BP(x,y1,y2,y3)DCO(x,z)TFx···西南石油大学计算机科学学院22不变式断言法实例建立检验条件：通路1：A-BI(x)=P(x,0,1,1)x0=0x1=(0+1)21=2*0+1通路2：B-D-BP(x,y1,y2,y3)y2x=p(x,y1+1,y2+y3+2,y3+2)y12xy2=(y1+1)2y3=2y1+1y2x=(y1+1)2xy2+y3+2=(y1+1+1)2y3+1=2(y1+1)+1通路3：B-CP(x,y1,y2,y3)y2x=O(x,y)y12xy2=(y1+1)2y3=2y1+1y2x=y12x(y1+1)2西南石油大学计算机科学学院23不变式断言法实例检验条件2y12xy2=(y1+1)2y3=2y1+1y2≤x=(y1+1)2≤xy2+y3+2=(y1+1+1)2y3+1=2(y1+1)+1证明：x≥(y1+1)2y2+y3+2=(y1+1)2+2y1+1+2=(y1+2)2y3+2=2y1+1+2=2(y1+1)+1检验条件3y12xy2=(y1+1)2y3=2y1+1y2x=y12≤x(y1+1)2证明：y12xxy2,y2=(y1+1)2=x(y1+1)2西南石油大学计算机科学学院24子目标断言法子目标断言法与不变式断言法的主要区别是：•两种方法对循环所建立的断言不同。不变式断言描述了程序变量y的中间值与初始值之间关系，而子目标断言法描述的是y的中间值与循环终止时的最终值yend之间的关系。•两种方法进行归纳的方向不同。不变式断言沿着程序正常执行的方向进行归纳，而子目标断言法则沿着相反方向进行归纳。西南石油大学计算机科学学院25不变式断言法输入断言：I(x,y):x00y00输出断言：O(x,y,z):z=gcd(x,y)循环不变式断言：P(x,y):x=0y=0gcd(x,y)=gcd(x0,y0)STARTRead(x,y)x0yxy:=y-xxyz:=ySTOPTFTFI(x,y)aP(x,y)bcO(x,y,z)deg•例：设x,y为正整数，求x,y的最大公约数z的程序，即z=gcd(x,y)。西南石油大学计算机科学学院26子目标断言法(建立断言)输入断言I(x,y):x00y00输出断言O(x,y,z):z=gcd(x,y)子目标断言(b为循环断点)P(x,y,yend):x=0y=0=yend=gcd(x,y)含义：每当控