程序设计方法学基本理论.ppt_第1页
程序设计方法学基本理论.ppt_第2页
程序设计方法学基本理论.ppt_第3页
程序设计方法学基本理论.ppt_第4页
程序设计方法学基本理论.ppt_第5页
已阅读5页,还剩17页未读 继续免费阅读

下载本文档

版权说明:本文档由用户提供并上传,收益归属内容提供方,若内容存在侵权,请进行举报或认领

文档简介

第五课 程序设计方法学基本理论 结构化程序的正确性证明,课件已上载至10/程序设计方法学(蔡铭),本课的内容,1.重复递归引理 2.正确性定理 3.结构化程序正确性证明的代数方法 4.循环不变式产生的方法,结构化程序正确性证明思路,任何结构化程序都可以用序列、条件和循环3种结构表示,其中循环的正确性最为复杂,若能够用序列和条件结构来表示循环,则可以使正确性证明得以简化。,重复递归引理(1/5),基本概念:基于程序函数的程序正确性概念。 假设已知一个程序P和一个预期函数F,若有 f=P 则称程序P正确地实现了函数f,或说程序P是正确的。,重复递归引理(2/5),重复递归引理内容 引理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;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 ,重复递归引理告诉我们,循环程序的验证可以通过将循环化为递归的方法,转化为终止性和由选择以及序列组成的无循环程序进行验证!,正确性定理(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(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,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,则可以建立赋值表如下:,分析跟踪表可知: 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,代数方法例子,于是有: 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(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)=(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+q a-a/b*b=a0

温馨提示

  • 1. 本站所有资源如无特殊说明,都需要本地电脑安装OFFICE2007和PDF阅读器。图纸软件为CAD,CAXA,PROE,UG,SolidWorks等.压缩文件请下载最新的WinRAR软件解压。
  • 2. 本站的文档不包含任何第三方提供的附件图纸等,如果需要附件,请联系上传者。文件的所有权益归上传用户所有。
  • 3. 本站RAR压缩包中若带图纸,网页内容里面会有图纸预览,若没有图纸预览就没有图纸。
  • 4. 未经权益所有人同意不得将文件中的内容挪作商业或盈利用途。
  • 5. 人人文库网仅提供信息存储空间,仅对用户上传内容的表现方式做保护处理,对用户上传分享的文档内容本身不做任何修改或编辑,并不能对任何下载内容负责。
  • 6. 下载文件中如有侵权或不适当内容,请与我们联系,我们立即纠正。
  • 7. 本站不保证下载资源的准确性、安全性和完整性, 同时也不承担用户因使用这些下载资源对自己和他人造成任何形式的伤害或损失。

评论

0/150

提交评论