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

* * * * * * * * * * * * * * * * * * * * * * 第6章 结构化程序的正确性证明 本课的内容 1.重复递归引理 2.正确性定理 3.结构化程序正确性证明的代数方法 4.循环不变式产生的方法 结构化程序正确性证明思路 任何结构化程序都可以用序列、条件和循环3种结构表示，其中循环的正确性最为复杂，若能够用序列和条件结构来表示循环，则可以使正确性证明得以简化。 重复递归引理 基本概念：基于程序函数的程序正确性概念。 假设已知一个程序P和一个预期函数f，若有 f=[P] 则称程序P正确地实现了函数f，或说程序P是正确的。 第二章中程序函数的定义 重复递归引理 重复递归引理内容 引理1 while-do的正确性定理 引理2 do-until的正确性定理 引理3 do-while-do的正确性定理 重复递归引理－－引理1 已知预期函数f和循环程序P while p do g 则f=[P]的充要条件是：对所有x∈D (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 ]= [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 引理2 已知函数f和循环程序P：do g until p ，则 f=[P]的充要条件是：对所有x∈D(f)，程序P终止，且 f=[g;if ?p then f ] 引理3 已知函数f和循环程序P：do1 g while p do2 h ,则 f=[P]的充要条件是：对所有x∈D(f)，程序P终止，且 f=[g;if p then h;f ] 重复递归引理告诉我们，循环程序的验证可以通过将循环化为递归的方法，将程序转化为由选择以及序列组成的无循环程序进行验证！ 正确性定理 已知预期函数f和基本程序P，则f=[P]的充要条件是： x∈D(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?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=x} = f 情形e,f由引理2，3可证 结构化程序正确性证明的代数方法 给定一个程序P的预期程序函数f，若x∈D(f)，程序P是终止的，且通过正确性定理求解程序P的程序函数f’，若与预期函数f相等，则得证。 证明步骤： 1：程序P是终止的； 2：f和程序P的定义域相同； 3：通过正确性定理求解程序P的程序函数f’，与预期函