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

本课的内容




第1页/共19页
结构化程序正确性证明思路
任何结构化程序都可以用序列、条件和循环3种结构表示,其中循环的正确性最为复杂,若能够用序列和条件结构来表示循环,则可以使正确性证明得以简化。
第2页/共19页
重复递归引理
基本概念:基于程序函数的程序正确性概念。
假设已知一个程序P和一个预期函数f,若有
f = [P]
则称程序P正确地实现了函数f,或说程序P是正确的。
第3页/共19页
重复递归引理
重复递归引理内容
引理1 while-do的正确性定理
引理2 do-until的正确性定理
引理3 do-while-do的正确性定理
第4页/共19页
重复递归引理-引理1
引理1 已知预期函数f和循环程序P
while p do g
则 f = [P]的充要条件是:
对所有x∈D(f), 程序P终止,
且 f=[if p then g;f]
第5页/共19页
重复递归引理-引理1
证明:
必要性:
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 ]
第6页/共19页
重复递归引理-引理2/3
引理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 ]
重复递归引理告诉我们,循环程序的验证可以通过将循环化为递归的方法,转化为终止性和由条件以及序列组成的无循环程序进行验证!
第7页/共19页
正确性定理(1/2)
已知预期函数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 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=f۰h۰g(x) | p۰g(x)  y=g(x)}
第8页/共19页
正确性定理-证明(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可证
第9页/共19页
结构化程序正确性证明的代数方法
给定一个程序P的预期程序函数f,若x∈D(f),程序P是终止的,且通过正确性定理求解程序P的程序函数f′,若与预期函数f相等,则得证。
证明步骤:
1:程序P是终止的;
2:f和程序P的定义域相同;
3:通过正确性定理求解程序P的程序函数f′,与预期函数f相等。
对于相对简单直观的程序,可以直接使用代数方法计算程序函数。
对于复杂的序列和条件程序,循环程序的证明,可以采取跟踪表方法求解程序函数。
第10页/共19页