38第6章 结构化程序的正确性证明

第6章结构化程序的正确性证明本课的内容1.重复递归引理2.正确性定理3.结构化程序正确性证明的代数方法4.循环不变式产生的方法结构化程序正确性证明思路任何结构化程序都可以用序列、条件和循环3种结构表示，其中循环的正确性最为复杂，若能够用序列和条件结构来表示循环，则可以使正确性证明得以简化。重复递归引理基本概念：基于程序函数的程序正确性概念。假设已知一个程序P和一个预期函数f，若有f=[P]则称程序P正确地实现了函数f，或说程序P是正确的。第二章中程序函数的定义重复递归引理重复递归引理内容引理1while-do的正确性定理引理2do-until的正确性定理引理3do-while-do的正确性定理重复递归引理－－引理1已知预期函数f和循环程序Pwhilepdog则f=[P]的充要条件是：对所有x∈D（f），程序P终止，且f=[ifptheng;f]重复递归引理－－引理1证明：必要性f=[P]=[whilepdog]=f=[ifptheng;f][P]=[whilepdog]=[ifptheng;whilepdog]=[ifptheng;f]充分性f=[ifptheng;f]=f=[whilepdog][ifptheng;f]=[ifptheng;ifptheng;f]=[ifptheng;ifptheng;……(ifptheng)]=[ifptheng;ifptheng;……I]=[whilepdog]重复递归引理－引理2和引理3引理2已知函数f和循环程序P：doguntilp，则f=[P]的充要条件是：对所有x∈D（f），程序P终止，且f=[g;if¬pthenf]引理3已知函数f和循环程序P：do1gwhilepdo2h,则f=[P]的充要条件是：对所有x∈D（f），程序P终止，且f=[g;ifpthenh;f]重复递归引理告诉我们，循环程序的验证可以通过将循环化为递归的方法，将程序转化为由选择以及序列组成的无循环程序进行验证！正确性定理已知预期函数f和基本程序P，则f=[P]的充要条件是：x∈D(f)，程序P终止，且对于不同的基本程序，函数f分别满足下列关系：情形a，对于序列，p=g;h,有f={(x,y)|y=hg(x)}情形b，对于if-then程序，ifptheng，有f={(x,y)|p(x)y=g(x)|¬p(x)y=x}情形c，对于if-then-else，ifpthengelseh，有f={(x,y)|p(x)y=g(x)|¬p(x)y=h(x)}情形d，对while-do程序，whilepdog，有f={(x,y)|p(x)y=fg(x)|¬p(x)y=x}情形e，对于do-until程序，doguntilpod,有f={(x,y)|pg(x)y=g(x)|¬pg(x)y=fg(x)}情形f，对于do-while-do程序，do1gwhilepdo2hod，有f={(x,y)|pg(x)y=fhg(x)|¬pg(x)y=g(x)}正确性定理－－证明情形a,b,c由程序函数直接可得情形d,由下式可得（根据引理1）：对while-do程序,whilepdog，有[whilepdog]=[ifptheng;f]={(x,y)|p(x)y=fg(x)|¬p(x)y=x}=f情形e,f由引理2，3可证结构化程序正确性证明的代数方法给定一个程序P的预期程序函数f，若x∈D（f），程序P是终止的，且通过正确性定理求解程序P的程序函数f’，若与预期函数f相等，则得证。证明步骤：1：程序P是终止的；2：f和程序P的定义域相同；3：通过正确性定理求解程序P的程序函数f’，与预期函数f相等。对于相对简单直观的程序，可以直接使用代数方法计算程序函数。对于复杂的序列和条件程序、循环程序的证明，可以采取跟踪表方法求解程序函数。代数方法——跟踪表1.已知程序P：x:=x+y;y:=x-y;x:=x-y;求它的程序函数。假设变量x,y的初值是x0,y0，执行第一个赋值语句后变量值为x1,y1……，则可以建立赋值表如下：语句xy1x:=x+yx1=x0+y0y1=y02y:=x-yx2=x1y2=x1-y13x:=x-yx3=x2-y2y3=y2分析跟踪表可知：x3=x2-y2=x1-(x1-y1)=y1=y0y3=y2=x1-y1=x0+y0-y0=x0通过跟踪表法，可知程序P的程序函数为{(x,y),(y,x)}代数方法——跟踪表2.序列程序y:=ay:=x*y+by:=x*y+cy:=x*y+d跟踪表为：语句xy1y:=ax1=x0y1=a2y:=x*y+bx2=x1y2:=x1*y1+b3y:=x*y+cx3=x2y3:=x2*y2+c4y:=x*y+dx4=x3y4:=x3*y3+d代数方法——跟踪表所以，x4=x3=x2=x1=x0y4=x3*y3+d=x2*(x2*y2+c)+d=x1*(x1*(x1*y1+b)+c)+d=x0*(x0*(x0*a+b)+c)+d相应的程序函数为：(x,y=x,x*(x*(x*a+b)+c)+d)即y=ax3+bx2+cx+d分离规则条件语句ifpthengelseh可用条件规则表示出来(pg|¬ph)。为了证明条件语句的正确性，就需要比较预期函数f和条件规则是否相等。复合条件规则的化简(p1(q11r11|q12r12)|p2(q21r21|q22r22))(p1∧q11)r11|(p1∧q12)r12|(p2∧q21)r21|(p2∧q22)r22p1,p2是分离的，即p1∧p2为假。如果一个条件规则的所有谓词都是分离的，称它为分离规则。将条件规则化为分离规则在化简和比较条件规则时，分离规则比一般的条件规则使用更方便一些。一般的复合规则不一定能展开，但分离的复合规则总可以展开。一般的条件规则的前后顺序是不能交换的，而分离规则的顺序是可以交换的。讨论程序的正确性时，总是首先将条件规则化为分离规则。将条件规则化为分离规则对于任意的条件规则（p1r1|p2r2|p3r3|…）化为分离规则（p1r1|¬p1∧p2r2|¬p1∧¬p2∧p3r3|…）条件语句的正确性证明假设某一条语句的程序函数是分离规则：（p1r1|p2r2|p3r3）预期函数是f，由于f可以是赋值的形式，例如y:=f(x)的形式给出时，为了证明条件语句的正确性，需证明以下两点：(1)f(x)的定义域和分离规则式的定义域是相同的；(2)利用分离规则的谓词将f(x)的定义域分解，并有以下关系成立：p1(x)r1(x)=f(x)p2(x)r2(x)=f(x)p3(x)r3(x)=f(x)条件语句的正确性证明另外，当f是以条件规则的形式给出时，例如，是下列的分离规则(q1s1|q2s2)这时，要证明它和分离规则式相同，需要证明：(1)两个分离规则的定义域是相同的，即p1(x)Vp2(x)Vp3(x)=q1(x)Vq2(x)(2)两个分离规则中的谓词成对合取后，相应的结果是相同的：p1(x)∧q1(x)r1(x)=s1(x)p1(x)∧q2(x)r1(x)=s2(x)……p3(x)∧q1(x)r3(x)=s1(x)p3(x)∧q2(x)r3(x)=s2(x)例子1预期函数f=(x:=-x)程序P为ifx0thenx:=x-2*xelsex:=x+2*abs(x)[P]=(x0x:=x-2*x|x≤0x:=x+2*abs(x))证明(1)f和P的定义域均为整数，相同。(2)[P]是一个分离规则，且x0(x:=x-2*x)=(x:=-x)x≤0(x:=x+2*abs(x))=(x:=x+2*(-x))=(x:=-x)得证例子2已知预期函数f是（x,y,a是整数，且x≥0）{(x,y,a),(0,a*x+y,a)}程序P如下，其中x≥0：whilex≠0dox,y=x-1,y+a证明程序P是正确的，即f=[P]证明1：程序是终止的证明2：定义域相同证明3：f={(x,y)|p(x)y=fg(x)|¬p(x)y=x}，其中，p(x)=(x0),¬p(x)=(x=0)利用fg(x)的跟踪表证明3例子2于是有：x2=0∧y2=a0*(x0-1)+y0+a0=a0*x0+y0即当x0时x,y,a:=0,a*x+y,a;当x=0时x,y,a:=0,y,a=0,a*0+y,a因此可知，f＝{(x,y,a),(0,a*x+y,a)}，与预期函数相等，因此得证。语句xyx,y:=x-1,y+ax1=x0-1y1=y0+a0x,y,a:=0,a*x+y,ax2=0y2=a0*x1+y1循环不变式产生的方法对于程序部分正确性证明的不变式断言法，这一方法的关键是建立一个正确的不变式断言，对一般程序来说，不变式断言的建立主要依靠程序员对程序的理解，尚无系统的方法。但对结构化程序来说，如果已知它的程序函数，则可以根据不变式状态定理，来确定它的一个循环不变式。循环不变式产生的方法不变式状态定理：假设f=[whilep(x)dog(x)]，x0是初始值，则循环不变式q(x)为：f(x)=f(x0)证明：1.在进入循环时，f(x0)=f(x0)，因此q(x)成立。2.试证假设在每一次进入循环前q(x)成立，即f(x)=f(x0)，则执行循环后q(x)也成立，即证明p(x)∧q(x)=qg(x)由p(x)为真，及正确性定理f={(x,y)|p(x)y=fg(x)|¬p(x)y=x}可知即p(x)=(f(x)=fg(x))循环不变式产生的方法又进入循环前q(x)成立，即q(x)=(f(x0)=f(x))∴p(x)∧q(x)=(f(x0)=fg(x))而(f(x0)=fg(x))＝(fg(x)=f(x0))＝(f(g(x))=f(x0))＝q(g(x))(归纳假设q(x)=(f(x)=f(x0)))＝qg(x)∴p(x)∧q(x)=qg(x)循环不变式产生的方法同理可知如下定理：2假设f(x)=[dog(x)untilp(x)]，则该循环不变式q(x)为f(x)=fg(x0)3假设f(x)=[do1g(x)whilep(x)do2h(x)]，则该循环不变式q(x)为f(x)=fhg(x0)循环不变式产生的方法－－例1对于循环程序P：whilev≠0dou,v=u+1,v-1，其程序函数为{(u,v),(u+v,0)}，求其循环不变式。（设u、v0）对循环中所有变量，分别计算f(x)和f(x0)，列表如下：则循环不变式为f(x)=f(x0)=u+v=u0+v0xf(x)f(x0)uu+vu0+v0v00循环不变式产生的方法－－例2求程序P：whilea≥bdoa,q:=a-b,q+1的循环不变式该程序的程序函数为{(a,b,q),(a-[a/b]*b,b,[a/b]+q)}a-[a/b]*b=a0-[a0/b0]*b0（1）b=b0（2）[a/b]+q=[a0/b0]+q0（3）由(1)、(2)得：a0-a=b*(a0/b0-a/b)（4）由(3)得：a0/b0-a/b=q-q0（5）综合(4)、(5)得a0-a=b*(q-q0)a0=a+b*qxf(x)f(x0)aa-[a/b]*ba0-[a0/b0]*b0bbb0q[a/b]+q[a0/b0]+q0作业课本P190习题4（分离规则）5（跟踪表）6(1)