资源描述：
《程序设计方法学基本理论》由会员上传分享，免费在线阅读，更多相关内容在教育资源-天天文库。
1、第五课程序设计方法学基本理论 ——结构化程序的正确性证明课件已上载至ftp://10.11.11.110/程序设计方法学（蔡铭）本课的内容1.重复递归引理2.正确性定理3.结构化程序正确性证明的代数方法4.循环不变式产生的方法结构化程序正确性证明思路任何结构化程序都可以用序列、条件和循环3种结构表示，其中循环的正确性最为复杂，若能够用序列和条件结构来表示循环，则可以使正确性证明得以简化。重复递归引理（1/5）基本概念：基于程序函数的程序正确性概念。假设已知一个程序P和一个预期函数F，若有f=[P]则称程序P正确地实现了函数f，或说程序P是
2、正确的。重复递归引理（2/5）重复递归引理内容引理1while-do的正确性定理引理2do-until的正确性定理引理3do-while-do的正确性定理重复递归引理－引理1（3/5）引理1已知预期函数f和循环程序Pwhilepdog则f=[P]的充要条件是：对所有X∈D（f），程序P终止，且f=[ifptheng；f]重复递归引理－引理1（4/5）证明：必要性：f=[P]=[whilepdog]—>[ifptheng;f][p]=[whilepdog]=[ifptheng;whilepdog]=[ifptheng;f]充分性：[ifpt
3、heng;f]—>[whilepdog][ifptheng;f]=[ifptheng;ifptheng;f]=[ifptheng;ifptheng;……(ifptheng)]=[ifptheng;ifptheng;……I]=[whilepdog]重复递归引理－引理2/3（5/5）引理2已知函数f和循环程序P：doguntilp,则f=[P]的充要条件是：程序P终止，且f=[g;if～pthenf]引理3已知函数f和循环程序P：do1gwhilepdo2h,则f=[P]的充要条件是：程序P终止，且f=[g;ifpthenh;f]重复递归引理
4、告诉我们，循环程序的验证可以通过将循环化为递归的方法，转化为终止性和由选择以及序列组成的无循环程序进行验证！正确性定理（1/2）已知预期函数f和基本程序P，则f=[P]的充要条件是：X∈D（f），程序P终止，且对于不同的基本程序，函数f分别满足下列关系情形a：对于序列，p=g;h,有f={(x,y)
5、y=h*g(x)}情形b：对于if-then程序，ifpthengfi，有f={(x,y)
6、p(x)—>y=g(x)
7、~p(x)—>y=x}情形c：对于if-then-else，ifpthengelsehfi，有f={(x,y)
8、p(x)—>
9、y=g(x)
10、~p(x)—>y=h(x)}情形d：对while-do程序,whilepdogod，有f={(x,y)
11、p(x)—>y=f*g(x)
12、~p(x)—>y=x}情形e：对于do-until程序,doguntilpod,有f={(x,y)
13、p*g(x)—>y=g(x)
14、~p*g(x)->y=f*g(x)}情形f：对于do-while-do程序，do1gwhilepdo2hod，有f={(x,y)
15、p*g(x)—>y=g(x)
16、p*g(x)->y=g(x)}正确性定理-证明（2/2）情形a,b,c由程序函数直接可得情形d,由下式可得
17、（根据引理1）：对while-do程序,whilepdog，有[whilepdo]=[ifptheng;f]={(x,y)
18、p(x)—>y=f*g(x)
19、~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相等。对于相对简单直观的程序，可以直接使用代数方法计算程序函
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=y0Y3=y2=x1=y1=x0+y0-y0=x0通过跟踪表法，可知程序P的程序函数为
21、{(x,y),(y,x)}代数方法——例子（跟踪表）例：已知预期函数f是（x,y,a是整数，且x≥0）{(x,y,a),(0,a*x+y,a)}程序P如下，其中x≥0：whilex<>0dox
