程序设计方法学第三章程序正确性证明.ppt

什么样的程序才是正确的？如何来保证程序是正确的？ 程序规约Q{S}R 是一个逻辑表达式，其取值为真或假，其中取值为真的含义是指：给定一段程序S，若程序开始执行之前Q为真，S的执行将终止，且终止时R为真，则称为 “程序S，关于前置断言Q和后置断言R是完全正确的”。 部分正确：若对于每个使得Q(i)为真，并且程序S计算终止的输入信息i，R(i,S(i))都为真，则称程序S关于Q和R是部分正确的。 程序终止：若对于每个使得Q(i)为真的输入i，程序S的计算都终止，则称程序S关于Q是终止的。 完全正确：程序是部分正确，同时又是终止的。 程序正确性的证明方法分类 （1）证明部分正确性的方法 A. Floyd的不变式断言法 B. Manna的子目标断言法 C. Hoare的公理化方法 （2）终止性证明的方法 A. Floyd的良序集方法 B. Knuth的计数器方法 C.Manna等人的不动点方法 （3）完全正确性的方法 A. Hoare公理化方法的推广 B. Burstall的间发断言法 C. Dijkstra的弱谓词变换方法以及强验证方法 不变式断言法 证明步骤： 1、建立断言：建立程序的输入、输出断言，如果程序中有循环出现的话，在循环中选取一个断点，在断点处建立一个循环不变式断言 2、建立检验条件，将程序分解为不同的通路，为每一个通路建立一个检验条件，该检验条件为如下形式： I ∧ R = O,其中I为输入断言，R为进入通路的条件，O为输出断言 3、证明检验条件：运用数学工具证明步骤2得到的所有检验条件，如果每一条通路检验条件都为真，则该程序为部分正确的。 不变式断言法实例1 例：设x,y为正整数，求x,y的最大公约数z的程序，即z=gcd(x,y)。 不变式断言法实例1 例：设x,y为正整数，求x,y的最大公约数z的程序，即z=gcd(x,y)。 不变式断言法实例1(建立断言) 输入断言：I(x1,x2): x10?x20 输出断言：O(x1,x2,z): z=gcd(x1,x2) 循环不变式断言(断点选为b): P(x1,x2,y1,y2): x10 ? x20 ? y10 ? y20 ? gcd(y1,y2)=gcd(x1,x2) 不变式断言法实例1(建立检验条件) 检验条件： I ^ R = O 通路1：I(x1,x2)= P(x1,x2,y1,y2) (无条件) x10 ? x20 ＝ x10 ? x20 ? y10 ? y20 ? gcd(y1,y2)=gcd(x1,x2) 通路2：P(x1,x2,y1,y2) ? y1y2 ? y1y2 = P(x1,x2,y1-y2,y2) x10 ? x20 ? y10 ? y20 ? gcd(y1,y2)=gcd(x1,x2) ? y1y2 ? y1y2 =x10 ? x20 ? y1-y20 ? y20 ? gcd(y1-y2,y2)=gcd(x1,x2) 通路3：P(x1,x2,y1,y2) ? y1y2 ? y1y2 = P(x1,x2,y1,y2-y1) 通路4：P(x1,x2,y1,y2) ? y1=y2 = O(x1,x2,z) 不变式断言法实例1(证明检验条件) 通路1：无需证明 通路2： 前提：P(x1,x2,y1,y2) ? y1y2 ? y1y2 = P(x1,x2,y1-y2,y2) 即：x10 ? x20 ? y10 ? y20 ? gcd(y1,y2)=gcd(x1,x2) ? y1y2 ? y1y2 结论：x10 ? x20 ? y1-y20 ? y20 ? gcd(y1-y2,y2)=gcd(x1,x2) 证明：因为y1y2,所以y1-y20成立,因此有 gcd(y1-y2,y2)=gcd(y1,y2) =gcd(x1,x2) 得证 通路3: y2y1则gcd(y1,y2-y1)= gcd(y1,y2)=gcd(x1,x2) 通路4: z=y1=y2则gcd(y1,y2) =y1=y2,又因gcd(x1,x2)= gcd(y1,y2) 成立，所以 Z= gcd(x1,x2)成立 不变式断言法实例2 对任一给定的自然数x，计算z＝[ ]，即计算x的平方根取整 1＋3＋…(2n+1)=(n+1)2(定理) 设y1=n; y3=2×y1+1； y2= (y1+1)2; 输入断言：