结构化程序的正确性证明

1、第6章 结构化程序的正确性证明本课的内容n1.重复递归引理n2.正确性定理n3.结构化程序正确性证明的代数方法n4.循环不变式产生的方法结构化程序正确性证明思路n任何结构化程序都可以用序列、条件和循环3种结构表示，其中循环的正确性最为复杂，若能够用序列和条件结构来表示循环，则可以使正确性证明得以简化。重复递归引理n基本概念：基于程序函数程序函数的程序正确性概念。 假设已知一个程序P和一个预期函数预期函数f，若有f=P 则称程序P正确地实现了函数正确地实现了函数f，或说程序程序P是是正确正确的。第二章中程序函数的定义重复递归引理n重复递归引理内容引理1 while-do的正确性定理引理2 do-

2、until的正确性定理引理3 do-while-do的正确性定理重复递归引理引理1n已知预期函数f和循环程序P while p do g 则f=P的充要条件是：对所有xD (f)， 程序P终止，且f=if p then g;f重复递归引理引理1证明：必要性 f= P=while p do g = f=if p then g;f P=while p do g=if p then g; while p do g =if p then g;f 充分性 f=if p then g;f = f= while p do g if p then g;f =if p then g;if p then g;f

3、= if p then g;if p then g;(if p then g) = if p then g;if p then g;I = while p do g 重复递归引理引理2和引理3n引理引理2 已知函数f和循环程序P：do g until p ，则 f=P的充要条件是：对所有xD(f)，程序P终止，且 f=g;if p then f n引理引理3 已知函数f和循环程序P：do1 g while p do2 h ,则 f=P的充要条件是：对所有xD(f)，程序P终止，且 f=g;if p then h;f 重复递归引理告诉我们，循环程序的验证可以通过将循环化为递归的方法，将程序转化为

4、由选择以及序列组成的无循环程序进行验证！ 正确性定理n已知预期函数f和基本程序P，则f=P的充要条件是： xD(f)，程序P终止，且对于不同的基本程序，函数f分别满足下列关系：情形a，对于序列，p=g;h,有f=(x,y)|y=h g(x)情形b，对于if-then程序，if p then g，有 f=(x,y)|p(x) y=g(x) | p(x) y=x情形c，对于if-then-else，if p then g else h，有 f=(x,y)|p(x) y=g(x)| p(x) y=h(x)情形d，对while-do程序，while p do g，有 f=(x,y)|p(x) y=f

5、g(x)| p(x) y=x情形e，对于do-until程序，do g until p od,有 f=(x,y)|p g(x) y=g(x)| p g(x) y=f g(x)情形f，对于do-while-do程序，do1 g while p do2 h od，有 f=(x,y)|p g(x) y= f h g(x)| p g(x) y=g(x)正确性定理证明情形a,b,c由程序函数直接可得情形d,由下式可得（根据引理1）： 对while-do程序,while p do g ，有 while p do g = if p then g;f = (x,y)|p(x) y=f g(x)| p(x) y

6、=x = f 情形e,f由引理2，3可证结构化程序正确性证明的代数方法n给定一个程序P的预期程序函数f，若xD(f)，程序程序P是终止是终止的的，且通过正确性定理求解程序且通过正确性定理求解程序P的程序函数的程序函数f，若与预期若与预期函数函数f相等，则得证相等，则得证。n证明步骤： 1：程序P是终止的； 2：f和程序P的定义域相同； 3：通过正确性定理求解程序P的程序函数f，与预期函数f相等。n对于相对简单直观的程序，可以直接使用代数方法计算程序函数。n对于复杂的序列和条件程序、循环程序的证明，可以采取跟踪表跟踪表方法求解程序函数。代数方法跟踪表1.已知程序P：x:=x+y;y:=x-y;x

7、:=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)代数方法跟踪表2.序列程序 y:=a y:=x*y+by:=x*y+cy:= x*y+d跟踪表为：语句xy1y:=ax1=x0y1=a2y:=x*y+bx2=x1y2:

8、=x1*y1+b3y:=x*y+cx3=x2y3:=x2*y2+c4y:= x*y+dx4=x3y4:=x3*y3+d代数方法跟踪表所以，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分离规则n条件语句 if p then g else h 可用条件规则表示出来 (pg | ph)。n为了证明条件语句的正确性，就需要比较预期函数f和条件规则是否相等。复合条件规则的

9、化简n (p1 (q11 r11 | q12 r12 ) | p2 (q21 r21 | q22 r22 ) )n(p1 q11) r11 | (p1 q12) r12 | (p2 q21) r21 | (p2 q22) r22np1,p2是分离的，即p1 p2为假。n如果一个条件规则的所有谓词都是分离的，称它为分离规则。将条件规则化为分离规则n在化简和比较条件规则时，分离规则比一般的条件规则使用更方便一些。n一般的复合规则不一定能展开，但分离的复合规则总可以展开。n一般的条件规则的前后顺序是不能交换的，而分离规则的顺序是可以交换的。n讨论程序的正确性时，总是首先将条件规则化为分离规则。将条件

10、规则化为分离规则n对于任意的条件规则（p1 r1 | p2 r2 | p3 r3 | ）化为分离规则（p1r1 |p1p2r2|p1p2p3r3 | ）条件语句的正确性证明n假设某一条语句的程序函数是分离规则： （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)条件语句的正确性证明

11、n另外，当f是以条件规则的形式条件规则的形式给出时，例如，是下列的分离规则 (q1 s1 | q2 s2 )n这时，要证明它和分离规则式相同，需要证明：(1)两个分离规则的定义域是相同的，即p1(x)Vp2(x)Vp3(x) = q1(x)V q2(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为 if x0 then x:

12、=x-2*x else x:=x+2*abs(x)P=(x0 x:=x-2*x| x0 x:=x+2*abs(x)证明(1) f和P的定义域均为整数，相同。(2) P是一个分离规则，且x0 (x:=x-2*x) = (x:=-x)x0 (x:=x+2*abs(x)=(x:=x+2*(-x)=(x:=-x)得证例子2 已知预期函数f是（x,y,a是整数，且x0） (x,y,a),(0,a*x+y,a) 程序P如下，其中x0： while x0 do x,y=x-1,y+a 证明程序P是正确的，即f=P 证明1：程序是终止的（用x值的变化说明） 证明2：定义域相同 证明3：由正确性定理情形d 可得

13、 f=(x,y)|p(x) y=f g(x) | p(x) y=x，其中，p(x)=(x0), p(x)=(x=0) （1）利用f g(x)的跟踪表证明例子2p(x)=(x0)于是有： x2 =0 y2=a0*(x0-1)+y0+a0=a0* x0 +y0即当x0时 x,y,a :=0,a*x+y,a;（2） p(x)=(x=0) 当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*

14、x1 + y1循环不变式产生的方法 对于程序部分正确性证明的不变式断言法，这一方法的关键是建立一个正确的不变式断言，对一般程序来说，不变式断言的建立主要依靠程序员对程序的理解，尚无系统的方法。 但对结构化程序来说，如果已知它的程序函数，则可以根据不变式状态定理不变式状态定理，来确定它的一个循环不变式。循环不变式产生的方法不变式状态定理不变式状态定理：假设f=while p(x) do g(x) ， x0是初始值，则 循环不变式q(x)为：f(x) = f(x0)证明：1.在进入循环时， f(x0) = f(x0)，因此q(x)成立。2.试证假设在每一次进入循环前q(x) 成立，即f(x) =

15、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

16、)=do g(x) until p(x) ，则该循环不变式q(x)为 f(x)=f g(x0)3假设 f(x)=do1 g(x) while p(x) do2 h(x) ，则该循环不变式q(x)为 f(x)=f h g(x0)循环不变式产生的方法例1对于循环程序P：while v0 do u,v=u+1,v-1 ，其程序函数为(u,v),(u+v,0)，求其循环不变式。（设u、v0）对循环中所有变量，分别计算f(x)和f(x0)，列表如下：则循环不变式为f(x)=f(x0) = u+v= u0+v0 xf(x)f(x0)uu+vu0+v0 v00循环不变式产生的方法例2求程序P： while ab do a,q:=a-b,q+1 的循环不变式该程