程序正确性证明(上)

第六章程序正确性证明1.概述2.不变式断言法证明程序的部分正确性3.良序集方法证明程序的终止性4.Hoare公理学方法6.1概述•基本概念–非形式化的程序验证是靠程序员阅读理解程序完成的。–程序测试是指测试者特意挑出一批输入数据，通过运行程序，检查每个输入数据所对应的运行结果是否符合预期要求。–Dijkstra说过“程序测试只能证明程序有错，不能说明程序正确”。除非进行穷举行测试。–正确性证明是论证程序达到预期目的的一般性陈述，而该论证与程序输入数据的特定值无关，能够代表穷举性测试。程序正确性概念•定义1.如果对于每一个使得P(ā)为真，程序S计算都终止，称程序S对P是终止的。•定义2：对于满足P(ā)为真，且能够使程序S计算终止的每个ā，如果Q(ā,P(ā))为真，则称程序S对于P和Q是部分正确的。•定义3：对于满足P(ā)为真的每个ā，如果程序S能够计算终止，且Q(ā,P(ā))为真，则称程序S对于P和Q是完全正确的。主要的程序正确性证明方法（1）关于部分正确性证明的方法–Floyd的不变式断言法–Manna的子目标断言法–Hoare的公理化方法（2）关于终止性证明的方法–Floyd的良序集方法–Knuth的计数器方法–Manna等人的不动点方法（3）关于完全正确性的证明方法–Hoare的公理化方法（Manna、Pnueli）–Bustall的间发断言法–Dijkstra的弱谓词转换方法以及强验证方法。中间断言•定义1：在程序任一中间点i附上谓词,如果每当执行到达i时对于该点的当前值必为真，则称为i点上的中间断言。•定义2：对于循环路径上的断言，因为每次循环执行到达该点时该断言必为真，所以该断言又称为循环不变式，简称不变式。),(yxpi),(yxpi),(yxpi6.2不变式断言法--证明部分正确性P(x)ρ(x,y)AQ(x,z)fgpBDE断言hC6.2不变式断言法--证明部分正确性证明步骤（分三步）1）建立断言：选取断点，建立断言2）建立检验条件3）验证检验条件1）建立断言：选取断点，建立断言–建立输入断言–建立输出断言，–若有循环，在循环通路中选取一个断点来“分割”循环，并在此建立一个适当的断言6.2不变式断言法--证明部分正确性P(x)ρ(x,y)AQ(x,z)fgpBDEhC6.2不变式断言法--证明部分正确性•2）建立检验条件–程序的执行可以分解为几条有限的通路–对每一条通路建立一个检验条件。)),(,(),(),(yxxyxyxrQRPiiiiP(x)ρ(x,y)AQ(x,z)fgpBDEhCAfBgpBEpBDhC6.2不变式断言法--证明部分正确性•“检验条件”是程序运行通过通路时应满足的条件。具体地说，将每一条通路看作一段程序–它的输入断言、输出断言分别和–而且通过此通路的条件为–通过此通路后y的值变为),(yxPi),(yxQi),(yxRi),(yxri)),(,(),(),(yxxyxyxrQRPiiii6.2不变式断言法--证明部分正确性•输入断言、输出断言分别和•而且通过此通路的条件为•通过此通路后y的值变为),(yxPi),(yxQi),(yxRi),(yxriP(x)ρ(x,y)AQ(x,z)fgpBDEhCAfBgpBEpBDhC6.2不变式断言法--证明部分正确性3）验证检验条件–验证（2）中得到的所有的检验条件，如果每一通路的检验条件均为真，则该程序是部分正确的)),(,(),(),(yxxyxyxrQRPiiii6.2不变式断言法举例例：设x1,x2是正整数，求它们的最大公约数，即z=gcd(x1,x2)其流程图程序如右图：关于最大公约数的性质：IFy1y20thengcd(y1,y2)=gcd(y1-y2,y2)IFy2y10thengcd(y1,y2)=gcd(y1,y2-y1)IFy2=y10theny1=y2=gcd(y1,y2)P(x)ρ(x,y)Q(x,z)x1,x2y1,y2GCABEy1=y2y1y2y1-y2y1y2-y1y2开始DYNYNy1z结束1)建立断言P(x)ρ(x,y)Q(x,z)x1,x2y1,y2GCABEy1=y2y1y2y1-y2y1y2-y1y2开始DYNYNy1z结束证明：•1)建立断言：–输入断言P(x)：–x10andx20–输出断言Q(x,z):–z=gcd(x1,x2)–不变式断言(x,y):x10∧x20∧y10∧y20∧gcd(x1,x2)=gcd(y1,y2)2)建立检验条件P(x)ρ(x,y)Q(x,z)x1,x2y1,y2GCABEy1=y2y1y2y1-y2y1y2-y1y2开始DYNYNy1z结束•根据图中选择的切点，程序有四条通路：–a1:AB–a2:BDB–a3:BEB–a4:BGC2)建立检验条件P(x)ρ(x,y)Q(x,z)x1,x2y1,y2GCABEy1=y2y1y2y1-y2y1y2-y1y2开始DYNYNy1z结束分别建立检验条件通路a1:AB•R1(x,y)=True•r1(x,y)=(x1,x2)•检验条件：•P(x)∧R1(x,y)(x,r1(x,y))...(1))),(,(),(),(yxxyxyxrQRPiiii2)建立检验条件P(x)ρ(x,y)Q(x,z)x1,x2y1,y2GCABEy1=y2y1y2y1-y2y1y2-y1y2开始DYNYNy1z结束分别建立检验条件通路a2(BDB):R2(x,y)=(y1neqy2andy1y2)r2(x,y)=(y1-y2,y2)检验条件：(x,y)andR2(x,y)(x,r2(x,y))...(2))),(,(),(),(yxxyxyxrQRPiiii分别建立检验条件•通路a3(BEB):–R3(x,y)=(y1neqy2andy1≤y2)–r3(x,y)=(y1,y2-y1)–检验条件：(x,y)andR3(x,y)(x,r3(x,y))...(3)•通路a4(BGC):–R4(x,y)=(y1=y2)–r4(x,z)=(y1)–检验条件：(x,y)andR4(x,y)Q(x,r4(x,z))...(4)3)证明检验条件•将上面建立的四个检验条件展开，证明它们为真–R1(x,y)=True–r1(x,y)=(x1,x2)–检验条件：•P(x)andR1(x,y)(x,r1(x,y))...(1)(x10∧x20∧True)(x10∧x20∧x10∧x20∧gcd(x1,x2)=gcd(x1,x2))...(1)–P(x):x10andx20–Q(x,z):z=gcd(x1,x2)–(x,y):x10∧x20∧y10∧y20∧gcd(x1,x2)=gcd(y1,y2)–(x10∧x20∧y10∧y20∧gcd(x1,x2)=gcd(y1,y2)∧y1≠y2∧y1y2)(x10∧x20∧y1-y20∧y20∧gcd(x1,x2)=gcd(y1-y2,y2))..(2)–(x10∧x20∧y10∧y20∧gcd(x1,x2)=gcd(y1,y2)∧y1≠y2∧y1≤y2)(x10∧x20∧y10∧y2-y10∧gcd(x1,x2)=gcd(y1,y2-y1))..(3)–(x10∧x20∧y10∧y20∧gcd(x1,x2)=gcd(y1,y2)∧y1=y2(y1=gcd(x1,x2))...(4)•结论：综上所述，该流程图程序是部分正确的。3)证明检验条件6.2不变式断言法--证明部分正确性3.通路条件Ri(x,y)和变换函数ri(x,y)的求法1）通路条件Ri(x,y)是指从穿过从i到j这条路径的条件2）变换函数ri(x,y)描述了当这条路径被穿过后，程序变量值的改变。3）求Ri(x,y)和ri(x,y)的反向代换技术：从割点i到j的路径a，反向代换技术为：a.开始，置Ri(x,y)=True,ri(x,y)为y，两者附着在割点j上b.根据下面的构造R和r的规则，由j向i反向移动。在割点i上得到的最终的R和r就是所求的Ri(x,y)和ri(x,y).c.构造R和r的规则如下：6.2不变式断言法--证明部分正确性c.构造R和r的规则如下：y=f(x)老新R(x,f(x))r(x,f(x))R(x,y)r(x,y)y=g(x,y)老新R(x,g(x,y))r(x,g(x,y))R(x,y)r(x,y)老新R(x,y)∧t(x,y)r(x,y)R(x,y)r(x,y)老新R(x,y)∧t(x,y)r(x,y)R(x,y)r(x,y)t(x,y)Tt(x,y)F6.2不变式断言法--证明部分正确性•c.构造R和r的规则如下(续)：新R(x,y)r(x,y)老R(x,y)r(x,y)6.2不变式断言法--证明部分正确性4)例：考虑下图，求该路径的路径函数R和ry=g1(x,y)step1:Step2:R:Tr:g3(x,y)R:Tr:yFt1(x,y)y=g2(x,y)t2(x,y)Ty=g3(x,y)Step3:R:t2(x,y)r:g3(x,y)Step4:R:t2(x,g2(x,y))r:g3(x,g2(x,y))Step5:R:t1(x,y)∧t2(x,g2(x,y))r:g3(x,g2(x,y))Step6:R:t1(x,g1(x,y))∧t2(x,g2(x,g1(x,y)))r:g3(x,g2(x,g1(x,y)))不变式断言法部分正确性证明算法step1:描述程序P的规范，即P和Q；step2:编写程序P；step3:为程序P选取割点集合，使每条循环均被割断step4:为P提供每个割点的中间断言step5:对P中每条不含中间割点的路径ai：•求该路径的Rai和rai;•写出该路径的检验条件•证明检验条件为真step6:由于下列任一理由，该程序得不到证明：•所提供得一个或几个断言不正确，返回Step4或3；•编写的程序有错，返回Step2•在使用机器证明情况下，可能超过机器的验证能力，而无法验证正确的检验条件的正确性课堂练习•对任一给定的自然数x，计算z=sqrt(x)的程序流程图如右。该程序的算法基于：对于任意整数n=0,有：1+3+5+(2n+1)=(n+1)2P(x):x=0Q(x,y):z2≤x(z+1)2p(x,y):y12≤x∧y2=(y1+1)2∧y3=(2y1+1)开始0,0,1y1,y2,y3y2x?y1z结束P(x)Ap(x,y)FBTDGCQ(x,z)y2+y3y2Fy1+1,y3+2y1,y3练习提示A--F:R(x,y):Truer(x,y)=(0,1,1)F--D--F:R(x,y):y2=xr(x,y)=(y1+1,y2+y3+2,y3+2)F--G--C:R(x,y):y2xr(x,z)=y16.3证明终止性的良序集方法•基本思想{0，1，2，3，4，5，6，7}界函数偏序集•设A是一个集合，如果A上的一个关系R，满足自反性、反对称性和传递性，则称R是A上的一个偏序关系。•在实数集上，≤就是一个偏序关系–自反性：a≤a–反对称性：若a≤b且b≤a，则必有a=b–传递性：若a≤b且b≤c，则必有a≤c良序集•任一偏序集合，假如它的每一个非空子集存在最小元素，这种偏序集称为良序的。•用另一种方式定义：–设（W,--）是一个偏序集，如果不存在由W中的元素构成的无限递减序列a0--a1--a2--...–称（W,--）是一个良序集。利用良序集方法证明程序的终止性设程序S的输入断言为P(x),利用良序集方法证明S关于P(x)是终止的步骤：1）选择一个割点集合，去截断程序的各个循环部分，并在每一个截点i处建立一个中间断言qi(x,y)。这样程序被分成若干个通路，同时规定每一通路都不含中间截断点。2）选取一个良序集（W,--),