程序正确性证明(下)

6.4程序正确性验证–Hoare公理学方法Hoare公理学方法•1969年提出了一种新的程序验证的方法。•使用了简洁的符号，提出了定义程序语义的公理系统。•Hoare系统是一个关于形如[P]S[Q]的断言的逻辑系统。–[P]S[Q]部分正确性断言–{P}S{Q}完全正确性断言•这个方法是针对WHILE型程序提出的。C.A.R.Hoare1.WHILE型程序WHILE型程序是由一个有限的语句序列组成，每个语句之间用分号隔开，即：B0；B1；...Bn其中，B0是程序中唯一的开始语句：STARTyf(x)Bi(1=i=n)是下列语句之一：1)赋值语句：yg(x,y)2)条件语句：ifRthenF1elseF2或ifRthenF13)复合：BeginF1，F2，...，FnEnd4)循环语句：whileRdoF15)停机语句：Zh(x,y)HALT其中，语句R是逻辑表达式，F1，F2，...，Fn是上列语句中的任何一种。1.WHILE型程序•例如：计算Z=sqrt(x)的程序：START(y1,y2,y3)(0,1,1);while(y2=x)do(y1,y2,y3)(y1+1,y2+y3+2,y3+2);Zy1;HALT1.WHILE型程序2.不变式演绎系统—Hoare系统•基本概念–不变式语句:[P]F[Q]•其中，P,Q是逻辑表达式，F是一个程序段。•他的含义是:“如果执行F以前P成立，且执行终止，则执行F后Q成立”,这时不变式语句为真，有时也称为归纳表达式。–推理规则•其中，B是一个不变式语句•Ai（i=1,2,…,n）是一个逻辑表达式或者是其它的不变式语句。•它的含义：“为了推导后项为真，只需证明前项A1,A2,…,An为真”.BAAAn,,,11引理：采用上述记号,一个程序S关于其输入断言P(x)和输出断言Q(x,z)的部分正确性可以表示为:[P(x)]S[Q(x,z)]因而，证明程序S的部分正确性,就可以归结为证明这一归纳表达式为真。2.不变式演绎系统—Hoare系统Hoare公理及其推理规则(1)赋值公理[P(x,g(x,y))]yg(x,y)[P(x,y)](2)条件规则[PR]F1[Q],[P¬R]F2[Q][P]ifRthenF1elseF2[Q]或者:[PR]F1[Q],P¬RQ[P]ifRthenF1[Q](3)While规则PI,[IR]F[I],I¬RQ[P]whileRdoF[Q](4)并置规则[P]F1[P1],[P1]F2[Q][P]F1;F2[Q](5)结论规则PR,[R]F[Q][P]F[Q]或者:[P]F[R],RQ[P]F[Q]Hoare系统的公理及其推理规则派生规则(1)赋值规则P(x,y)Q(x,g(x,y))[P(x,y)]yg(x,y)[Q(x,y)](2)重复赋值规则P(x,y)Q(x,gn(x,gn-1(x,…,g2(x,g1(x,y))…)))[P(x,y)]yg1(x,y);yg2(x,y);…;ygn(x,y);[Q(x,y)](3)变形并置规则[P]F1[Q],[R]F2[S],QR[P]F1;F2[S]两种证明方法•证明程序部分正确性的公理学方法就是依据以上公理和推理规则进行的，一般有两种形式：•正向“证明”–从某些公理出发，经使用规则，直到最后获得结果。•反向“证明”–先用规则，把总目标分成若干子目标，最后寻根于公理。正向证明过程•从某些公理出发，经使用规则，直到最后获得结果：–根据给出的不变式断言，建立一些引理。–根据引理和赋值公理，对程序中S的每一个赋值语句Fi导出相应的不变式语句[Ri]Fi[Qi]。–再根据这些不变式语句和上述的推理规则，逐步组成越来越长的程序段。–一直到推演出：[P(x)]F[Q(x,z)]为止。正向证明举例例1：证明z=sqrt(x)的程序的部分正确性：START[P(x):x=0}(y1,y2,y3)(0,1,1);While(y2=x)do[p(x,y):y12=xandy2=(y1+1)2andy3=2*y1+1}(y1,y2,y3)(y1+1,y2+y3+2,y3+2);Zy1;[Q(x,z):z2=x(z+1)2}HALT1)首先建立引理：引理1：x≥0p(x,0,1,1)………………(1)引理2：p(x,y)y2≤xp(x,y1+1,y2+y3+2,y3+2)…(2)引理3：p(x,y)y2xQ(x,y1)…………(3)这3个引理实质上就是前面提到的几个通路的检验条件，前面已经证明他们是正确的。)),(,(),(),(yxxyxyxrQRPiiii正向证明举例课堂练习•对任一给定的自然数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,y36.2不变式断言法--证明部分正确性•2）建立检验条件–程序的执行可以分解为几条有限的通路，对每一条通路建立一个检验条件。–“检验条件”是程序运行通过通路时应满足的条件。具体地说：若将每一条通路看作一段程序，它的输入断言、输出断言分别为，而且通过此通路的条件为，通过此通路后y的值变为，则相应的经验条件为：),(yxPi),(yxQi),(yxRi),(yxri)),(,(),(),(yxxyxyxrQRPiiii2)根据赋值公理有：[p(x,0,1,1)](y1,y2,y3)(0,1,1)[p(x,y)]……(4)根据式(1),(4)结论得：[x≥0](y1,y2,y3)(0,1,1)[p(x,y)]……(5)赋值公理:[P(x,g(x,y))]yg(x,y)[P(x,y)]正向证明举例x≥0p(x,0,1,1)…(1)3)根据赋值公理有：[p(x,y1+1,y2+y3+2,y3+2)](y1,y2,y3)(y1+1,y2+y3+2,y3+2)[p(x,y)]…(6)根据式(2),(6)结论得：[p(x,y)y2≤x](y1,y2,y3)(y1+1,y2+y3+2,y3+2)[p(x,y)]…(7)正向证明举例赋值公理:[P(x,g(x,y))]yg(x,y)[P(x,y)]p(x,y)y2≤xp(x,y1+1,y2+y3+2,y3+2)…(2)4)取I为p(x,y),Q为p(x,y)y2x，有：pI,p(x,y)y2xQ…..(8)根据式(7),(8),由while规则得：[p(x,y)]While(y2=x)do(y1,y2,y3)(y1+1,y2+y3+2,y3+2);[p(x,y)y2x]………..(9)正向证明举例While规则:PI,[IR]F[I],I¬RQ[P]whileRdoF[Q][p(x,y)y2≤x](y1,y2,y3)(y1+1,y2+y3+2,y3+2)[p(x,y)]…(7)5)根据并置规则，将(5)式、(9)式并置有：[x≥0](y1,y2,y3)(0,1,1);While(y2=x)do(y1,y2,y3)(y1+1,y2+y3+2,y3+2);[p(x,y)y2x]………………（10）正向证明举例并置规则[P]F1[P1],[P1]F2[Q][P]F1;F2[Q][x≥0](y1,y2,y3)(0,1,1)[p(x,y)]……(5)6）[Q(x,y1)]Zy1[Q(x,z)](赋值公理)得：[p(x,y)y2x]Zy1[Q(x,z)]…(11)7）由(10),(11)得：[x=0](y1,y2,y3)(0,1,1);While(y2=x)do(y1,y2,y3)(y1+1,y2+y3+2,y3+2);Zy1;[Q(x,z)][证明完毕]正向证明举例赋值公理:[P(x,g(x,y))]yg(x,y)[P(x,y)]反向证明过程•先用规则，把总目标分成若干子目标，最后寻根于公理：–从不变式语句[P(x)]F[Q(x,z)]出发–利用有关的规则将它逐步分解–一直到将所有的语句推演为逻辑表达式(即检验条件)–然后证明这些逻辑表达式成立–这样就证明了程序的部分正确性.反向证明举例例2：利用Hoare公理化方法证明程序的部分正确性START[P(X):x0≥0∧y0≥0∧x0≠0∨y0≠0]x,yx0,y0;whilexneq0do[p(x,y):x≥0∧y≥0∧(x0≠0∨y0≠0)∧(gcd(x,y)=gcd(x0,y0)]ify≥xthenyy-x;elses,x,yx,y,s;[y=gcd(x0,y0)]zy;[Q(x,z):z=gcd(x0,y0)]HALT反向证明要证明程序A的部分正确性，只要证明：Goal1:[P(x)]BodyA[Q(x,z)]1.1[P(x)]x,yx0,y0[p(x,y)]1.1.1P(x)p(x0,y0).............(1)1.2[p(x,y)]whilex≠0doify≥xtheny=y-xelses,x,yx,y,s;[y=gcd(x0,y0)]1.3[y=gcd(x0,y0)]zy[Q(x,z)]1.3.1y=gcd(x0,y0)Q(x,y)..........(2)1.2[p(x,y)}whilex≠0doify≥xtheny=y-xelses,x,yx,y,s;[y=gcd(x0,y0)]1.2.1[p(x,y)∧x≠0]ify≥xtheny=y-xelses,x,yx,y,s[p(x,y)]1.2.1.1[p(x,y)∧x≠0∧y≥x]y=y-x[p(x,y)]1.2.1.1.1[p(x,y)∧x≠0∧y≥x}p(x,y-x)...(3)1.2.1.2[p(x,y)∧x≠0∧yx]s,x,yx,y,s[p(x,y)]1.2.1.2.1[p(x,y)∧x≠0∧yx]p(y,x).......(4)1.2.2(p(x,y)∧x=0)(y=gcd(x0,y0))....................(5)最后，只要证明上面最后得到的5个谓词表达式为真即可反向证明反向证明过程讨论•反向证明过程开始于寻找一条适当规则W1,W2,…,WnW•把证明目标W分解为子目标W1,W2,…,Wn,然后又把子目标Wi用同样的方法再细分，直至最后的子目标或归根于公理或问底于论域的定理。这个过程的每一步可用图表示为：WW1W2W3…Wn练习•1.用反向证明方法证明例1.•2.用正向证明方法证明例2.