《程序设计方法学基本理论.ppt》由会员分享，可在线阅读，更多相关《程序设计方法学基本理论.ppt（22页珍藏版）》请在三一办公上搜索。
1、第五课 程序设计方法学基本理论 结构化程序的正确性证明,课件已上载至ftp:/10.11.11.110/程序设计方法学（蔡铭）,本课的内容,1.重复递归引理2.正确性定理3.结构化程序正确性证明的代数方法4.循环不变式产生的方法,结构化程序正确性证明思路,任何结构化程序都可以用序列、条件和循环3种结构表示，其中循环的正确性最为复杂，若能够用序列和条件结构来表示循环，则可以使正确性证明得以简化。,重复递归引理（1/5）,基本概念：基于程序函数的程序正确性概念。假设已知一个程序P和一个预期函数F，若有 f=P 则称程序P正确地实现了函数f，或说程序P是正确的。,重复递归引理（2/5）,重复递归引理
2、内容引理1 while-do的正确性定理引理2 do-until的正确性定理引理3 do-while-do的正确性定理,重复递归引理引理1（3/5）,引理1 已知预期函数f和循环程序P while p do g 则 f=P的充要条件是：对所有XD（f），程序P终止，且 f=if p then g；f,重复递归引理引理1（4/5）,证明：必要性：f=P=while p do g if p then g;f p=while p do g=if p then g;while p do g=if p then g;f 充分性：if p then g;f while p do g if p then g
3、;f=if p then g;if p then g;f=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/3（5/5）,引理2 已知函数f和循环程序P：do g until p,则 f=P的充要条件是：程序P终止，且 f=g;if p then f 引理3 已知函数f和循环程序P：do1 g while p do2 h,则 f=P的充要条件是：程序P终止，且 f=g;if p then h;f,重复递归引理告诉我们，循环程序的验证可以通过将循环化为递归的方法，转化为终止
4、性和由选择以及序列组成的无循环程序进行验证！,正确性定理（1/2）,已知预期函数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 fi，有 f=(x,y)|p(x)y=g(x)|p(x)y=x情形c：对于if-then-else，if p then g else h fi，有 f=(x,y)|p(x)y=g(x)|p(x)y=h(x)情形d：对while-do程序,while p do g od，有 f=(x,y)|p(
5、x)y=f*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=g(x)|p*g(x)-y=g(x),正确性定理-证明（2/2）,情形a,b,c由程序函数直接可得情形d,由下式可得（根据引理1）：对while-do程序,while p do g，有 while p do=if p then g;f=(x,y)|p(x)y=f*g(x)|p(x)y=x=f 情形e
6、,f由引理2，3可证,结构化程序正确性证明的代数方法,给定一个程序P的预期程序函数f，若XD（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，
7、则可以建立赋值表如下：,分析跟踪表可知：X3=x2-y2=x1-(x1-y1)=y1=y0 Y3=y2=x1=y1=x0+y0-y0=x0通过跟踪表法，可知程序P的程序函数为(x,y),(y,x),代数方法例子（跟踪表）,例：已知预期函数f是（x,y,a是整数，且x0）(x,y,a),(0,a*x+y,a)程序P如下，其中x 0：while x0 do x,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,
8、代数方法例子,于是有：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)，与预期函数相等，因此得证。,循环不变式产生的方法,对于程序部分正确性证明的不变式断言法，这一方法的关键是建立一个正确的不变式断言，对一般程序来说，不变式断言的建立主要依靠程序员对程序的理解，尚无系统的方法。但对结构化程序来说，如果已知它的程序函数，则可以根据不变式状态定理，来确定它的一个循环不变式。,循环不变式产生的方法,不变式状态定理：假设f=while p
9、(x)do g(x)，x0是初始值，则 循环不变式q(x)为：f(x)=f(x0)证明：1.在第一次进入循环时，f(x0)=f(x0)，因此q(x)成立。2.试证假设在每一次进入循环前q(x)成立，即f(x0)=f(x)，则执行循环后q(x)也成立，即证明 p(x)q(x)=q(g(x)=(f(g(x)=f(x0)由p(x)为真，以及正确性定理 f=(x,y)|p(x)y=f*g(x)|p(x)y=x可知 即 f(x0)=f(x)y=f*g(x)=f(g(x),循环不变式产生的方法,同理可知如下定理：2 假设 f(x)=do g(x)until p(x)，则该循环不变式q(x)为 f(x)=(
10、f(x)=f*g(x0)3假设 f(x)=do1 g(x)while p(x)do2 h(x),则该循环不变式q(x)为 f(x)=f*h*g(x),循环不变式产生的方法例1,对于循环程序P：while v0 do u,v=u+1,v-1 其程序函数为(u,v),(u+v,0)，求其循环不变式对循环中所有变量，分别计算f(x)和f(x0)，列表如下：则循环不变式为f(x)=f(x0)=u+v=u0+v0,循环不变式产生的方法例2,求程序P：while ab do a,q:=a-b,q+1 的循环不变式该程序的程序函数为(a,b,q),(a-a/b*b),b,a/b+qa-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),程序正确性证明练习,P174页习题1和2P190页习题1和6,
