结构化程序的正确性证明.ppt

、条件和循环3种结构表示,其中循环的正确性最为复杂,若能够用序列和条件结构来表示循环,则可以使正确性证明得以简化。重复递归引理基本概念:基于程序函数的程序正确性概念。假设已知一个程序P和一个预期函数f,若有f=[P]则称程序P正确地实现了函数f,或说程序P是正确的。第二章中程序函数的定义重复递归引理重复递归引理内容引理1while-do的正确性定理引理2do-until的正确性定理引理3do-while-do的正确性定理重复递归引理--引理1已知预期函数f和循环程序Pwhilepdog则f=[P]的充要条件是:对所有x∈D(f),程序P终止,且f=[ifptheng;f]重复递归引理--引理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]重复递归引理-引理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]重复递归引理告诉我们,循环程序的验证可以通过将循环化为递归的方法,将程序转化为由选择以及序列组成的无循环程序进行验证!正确性定理已知预期函数f和基本程序P,则f=[P]的充要条件是:x∈D(f),程序P终止,且对于不同的基本程序,函数f分别满足下列关系:情形a,对于序列,p=g;h,有f={(x,y)|y=hg(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=fg(x)|¬p(x)y=x}情形e,对于do-until程序,doguntilpod,有f={(x,y)|pg(x)y=g(x)|¬pg(x)y=fg(x)}情形f,对于do-while-do程序,do1gwhilepdo2hod,有f={(x,y)|pg(x)y=fhg(x)|¬pg(x)y=g(x)}正确性定理--证明情形a,b,c由程序函数直接可得情形d,由下式可得(根据引理1):对while-do程序,whilepdog,有[whilepdog]=[ifptheng;f]={(x,y)|p(x)y=fg(x)|¬p(x)y=x}=f情形e,f由引理2,3可证