结构化程序的正确性证明

结构化程序的正确性证明第1页，共30页，2023年，2月20日，星期四本课的内容1.重复递归引理2.正确性定理3.结构化程序正确性证明的代数方法4.循环不变式产生的方法第2页，共30页，2023年，2月20日，星期四结构化程序正确性证明思路任何结构化程序都可以用序列、条件和循环3种结构表示，其中循环的正确性最为复杂，若能够用序列和条件结构来表示循环，则可以使正确性证明得以简化。第3页，共30页，2023年，2月20日，星期四重复递归引理基本概念：基于程序函数的程序正确性概念。

假设已知一个程序P和一个预期函数f，若有f=[P]

则称程序P正确地实现了函数f，或说程序P是正确的。第二章中程序函数的定义第4页，共30页，2023年，2月20日，星期四重复递归引理重复递归引理内容引理1while-do的正确性定理引理2do-until的正确性定理引理3do-while-do的正确性定理第5页，共30页，2023年，2月20日，星期四重复递归引理－－引理1已知预期函数f和循环程序Pwhilepdog则f=[P]的充要条件是：对所有x∈D（f），程序P终止，且f=[ifptheng;f]第6页，共30页，2023年，2月20日，星期四重复递归引理－－引理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]第7页，共30页，2023年，2月20日，星期四重复递归引理－引理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]重复递归引理告诉我们，循环程序的验证可以通过将循环化为递归的方法，将程序转化为由选择以及序列组成的无循环程序进行验证！

第8页，共30页，2023年，2月20日，星期四正确性定理已知预期函数f和基本程序P，则f=[P]的充要条件是：x∈D(f)，程序P终止，且对于不同的基本程序，函数f分别满足下列关系：情形a，对于序列，p=g;h,有f={(x,y)|y=hg(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=fg(x)|¬p(x)y=x}情形e，对于do-until程序，doguntilpod,有

f={(x,y)|pg(x)y=g(x)|¬pg(x)y=fg(x)}情形f，对于do-while-do程序，do1gwhilepdo2hod，有

f={(x,y)|pg(x)y=fhg(x)|¬pg(x)y=g(x)}第9页，共30页，2023年，2月20日，星期四正确性定理－－证明情形a,b,c由程序函数直接可得情形d,由下式可得（根据引理1）：对while-do程序,whilepdog，有

[whilepdog]=[ifptheng;f]={(x,y)|p(x)y=fg(x)|¬p(x)y=x}=f情形e,f由引理2，3可证第10页，共30页，2023年，2月20日，星期四结构化程序正确性证明的代数方法给定一个程序P的预期程序函数f，若x∈D（f），程序P是终止的，且通过正确性定理求解程序P的程序函数f’，若与预期函数f相等，则得证。证明步骤：1：程序P是终止的；2：f和程序P的定义域相同；3：通过正确性定理求解程序P的程序函数f’，与预期函数f相等。对于相对简单直观的程序，可以直接使用代数方法计算程序函数。对于复杂的序列和条件程序、循环程序的证明，可以采取跟踪表方法求解程序函数。第11页，共30页，2023年，2月20日，星期四代数方法——跟踪表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=y0

y3=y2=x1-y1=x0+y0-y0=x0通过跟踪表法，可知程序P的程序函数为{(x,y),(y,x)}第12页，共30页，2023年，2月20日，星期四代数方法——跟踪表2.序列程序

y:=a y:=x*y+b y:=x*y+c y:=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第13页，共30页，2023年，2月20日，星期四代数方法——跟踪表所以，

x4=x3=

x2=x1=x0

y4=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第14页，共30页，2023年，2月20日，星期四分离规则条件语句ifpthengelseh可用条件规则表示出来(pg|¬ph)。为了证明条件语句的正确性，就需要比较预期函数f和条件规则是否相等。第15页，共30页，2023年，2月20日，星期四复合条件规则的化简(p1

(q11r11|q12r12)| p2(q21r21|q22r22))(p1∧q11)r11|(p1∧q12)r12|(p2∧q21)r21|(p2∧q22)r22p1,p2是分离的，即p1∧

p2为假。如果一个条件规则的所有谓词都是分离的，称它为分离规则。第16页，共30页，2023年，2月20日，星期四将条件规则化为分离规则在化简和比较条件规则时，分离规则比一般的条件规则使用更方便一些。一般的复合规则不一定能展开，但分离的复合规则总可以展开。一般的条件规则的前后顺序是不能交换的，而分离规则的顺序是可以交换的。讨论程序的正确性时，总是首先将条件规则化为分离规则。第17页，共30页，2023年，2月20日，星期四将条件规则化为分离规则对于任意的条件规则（p1r1|p2r2

|p3r3|

…） 化为分离规则（p1r1|¬p1∧p2r2|¬p1∧¬p2∧p3r3|

…）第18页，共30页，2023年，2月20日，星期四条件语句的正确性证明假设某一条语句的程序函数是分离规则： （p1r1|p2r2|p3r3）预期函数是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)第19页，共30页，2023年，2月20日，星期四条件语句的正确性证明另外，当f是以条件规则的形式给出时，例如，是下列的分离规则(q1

s1|q2s2)这时，要证明它和分离规则式相同，需要证明：(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)第20页，共30页，2023年，2月20日，星期四例子1预期函数f=(x:=-x)程序P为ifx>0thenx:=x-2*xelsex:=x+2*abs(x)

[P]=(x>0x:=x-2*x|x≤0x:=x+2*abs(x)) 证明(1)f和P的定义域均为整数，相同。(2)[P]是一个分离规则，且x>0(x:=x-2*x)=(x:=-x)x≤0(x:=x+2*abs(x))=(x:=x+2*(-x))=(x:=-x) 得证第21页，共30页，2023年，2月20日，星期四例子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=fg(x)|¬p(x)y=x}， 其中，p(x)=(x>0),¬p(x)=(x=0)

利用fg(x)的跟踪表证明3第22页，共30页，2023年，2月20日，星期四例子2于是有：

x2=0∧y2=a0*(x0-1)+y0+a0=a0*x0+y0即当x>0时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+a0

x,y,a:=0,a*x+y,ax2=0y2=a0*x1+y1第23页，共30页，2023年，2月20日，星期四循环不变式产生的方法对于程序部分正确性证明的不变式断言法，这一方法的关键是建立一个正确的不变式断言，对一般程序来说，不变式断言的建立主要依靠程序员对程序的理解，尚无系统的方法。但对结构化程序来说，如果已知它的程序函数，则可以根据不变式状态定理，来确定它的一个循环不变式。第24页，共30页，2023年，2月20日，星期四循环不变式产生的方法不变式状态定理：假设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)=>qg(x)由p(x)为真，及正确性定理

f={(x,y)|p(x)y=fg(x)|¬p(x)y=x}可知即p(x)=>(f(x)=fg(x))第25页，共30页，2023年，2月20日，星期四循环不变式产生的方法又进入循环前q(x)成立，即q(x)=(f(x0)=f(x))∴p(x)∧q(x)=>(f(x0)=fg(x))而(f(x0)=fg(x))＝(fg(x)=f(x0))＝(f(g(x))=f(x0)) ＝q(g(x))(归纳假设q(x)=(f(x)=f(x0))) ＝qg(x)∴p(x)∧q(x)=>qg(x)第26页，共30页，2023年，2月20日，星期四循环不变式产生的方法同理可知如下定理：2假设

f(x)=[dog(x)untilp(x)]，则该循环不变式q(x)为

f(x)=fg(x0)3假设

f(x)=[do1g(x)whilep(x)do2h(x)]，则该循环不变式q(x)为

f(x)=fhg(x0)第27页，共30页，2023年，2月20日，星期四