第5章 程序正确性证明

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