利用HOARE公理化方法证明程序部分正确性

利用HOARE公理化方法证明程序部分正确性

张兆朋201313283614478009@Hoare的公理化方法背景：定义：[P]S[Q]不变式语句Hoare的公理化方法的证明规则赋值语句公理条件语句规则循环语句规则并置规则结论规则实例证明通过实例来演示Hoare公理化方法的证明过程程序正确性证明－Hoare的公理化方法

1969年，Hoare在Floyd的不变式断言法基础上，提出了一种证明程序部分正确性的Hoare公理化方法。根据结构化定理，他提出了顺序语句、条件语句、WHILE循环语句三种基本语句证明规则，试图建立一个不变式演绎系统，以达到程序证明自动化之目的。1990年IEEE计算机先驱奖1980年图灵奖英国牛津大学计算机科学家查尔斯.霍尔(CharlesAntonyRichardHoare)发明Quicksort算法、CASE语句1963年实现了Algol语言1969年1月，在Comm.OfACM上发表“AnAxiomaticbasisforComputerProgramming”,提出公理语义学操作系统的MonitorACM在1983年评出在近25年在CACM上发表的25篇里程碑式的论文25篇，2人2篇，Hoare是其一程序正确性证明－Hoare的公理化方法定义

不变式语句

称[P]S[Q]是不变式语句。其含义是：如果执行S之前P为真，并且S执行终止，Q为真，称不变式语句为真或称归纳表达式为真，证明程序S的部分正确性,就可以归结为证明这一归纳表达式为真.

Hoare公理系统的推理规则一般形式为：其中：B为不变式语句，是逻辑表达式或其他不变式语句，其含义是：为了推论B为真，只需证明前提Ai(i=1,2,…,n)为真。为了证明程序P关于输入条件I(x)与输出条件O(x,p(x))是部分正确的，归结为证明不变式语句[I(x)]P[O(x,P(x))]为真。程序正确性证明－Hoare的公理化方法Hoare提出的公理和相应控制语句的证明规则。1.赋值语句公理设有赋值语句y←f(x)，则其公理为：[P(x,f(x,y))]y←f(x)[P(x,y)]

程序正确性证明－Hoare的公理化方法Hoare提出的公理和相应控制语句的证明规则。2.条件语句规则

[P∧R]S1[Q],[P∧﹁R]S2[Q] [P]IFRTHENS1ELSES2[Q]

或

[P∧R]S[Q],[P∧﹁R]=>[Q] [P]IFRTHENS[Q]程序正确性证明－Hoare的公理化方法Hoare提出的公理和相应控制语句的证明规则。3.循环语句规则

P=>I,[I∧R]S[I],I∧﹁R=>Q [P]WHILERDOS

[Q]

此规则中的逻辑表达式I就是非形式证明中的循环不变式断言。条件P=>I表明，当控制进入循环时，循环不变式I应为真；不变式[I∧R]S[I]表明，如果执行S之前（R为真时才执行S）I为真，且S执行终止，则S执行后I仍为真；条件I∧﹁R=>Q表明，如果控制退出循环，Q应为真。程序正确性证明－Hoare的公理化方法Hoare提出的公理和相应控制语句的证明规则。4.并置规则

[P]S1[R],[R]S2[Q] [P]S1;S2[Q]程序正确性证明－Hoare的公理化方法Hoare提出的公理和相应控制语句的证明规则。5.结论规则

P=>R,[R]S[Q] [P]S[Q]

或

[P]S[R],R=>Q [P]S[Q]

程序正确性验证–Hoare公理学方法证明过程证明程序部分正确性的公理学方法就是依据以上的公理和推理规则,一般有两种形式:正向证明和反向证明正向“证明”:从某些公理出发,使用规则,直到最后获得结果.根据给出的不变式断言,建立一些引理;根据引理和赋值公理,对程序中的每一个赋值语句Fi导出相应的不变式语句[Ri]Fi[Qi];再根据这些不变式语句和上述的推理规则逐步地组成越来越长的程序段,一直到推演出:[P(x)]F[Q(x,z)]为止.程序正确性证明－Hoare的公理化方法练习：对任一给定的自然数x，计算z=sqrt(x)的程序流程图如右。该程序的算法基于：对于任意整数n>=0,有1+3+5+(2n+1)=(n+1)2P(x):x>=0Q(x,y):z2≤x<(z+1)2

p(x,y):y12≤x∧y2=(y1+1)2∧y3=(2y1+1)程序正确性证明－Hoare的公理化方法3.举例：例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);Zy1;[Q(x,z):z2<=x<(z+1)2]HALT开始0,1,1y1,y2,y3y2>x?y1+1,y2+y3+2,y3+2y1,y2,y3y1z结束P(x)AFB’TDGCFq(x,y1,y2,y3)7.4程序正确性验证–Hoare公理学方法正向证明：1)首先建立引理：引理1：P(x)P(x,0,1,1)…………….(1)引理2：P(x,y)y2≤xP(x,y1+1,y2+y3+2,y3+2)(2)引理3：P(x,y)y2>xQ(x,y1)…(3)(需要，并且可以证明他们是正确的)2)根据赋值公理有：

[P(x,0,1,1)]（y1,y2,y3）(0,1,1)[P(x,y)]…..(4)

得：[P(x)](y1,y2,y3)(0,1,1)[P(x,y)]…(5)(式1,4,结论)[P(x,y1+1,y2+y3+2,y3+2)](y1,y2,y3)(y1+1,y2+y3+2,y3+2)[P(x,y)]..(6)

得：[P(x,y)y2≤x](y1,y2,y3)(y1+1,y2+y3+2,y3+2)[P(x,y)]..(7)7.4程序正确性验证–Hoare公理学方法4)取I为P(x,y),Q为P(x,y)y2>x，有：

PI,P(x,y)y2>xQ…..(8)

得：[P(x,y)]While(y2<=x)do(y1,y2,y3)(y1+1,y2+y3+2,y3+2);[P(x,y)y2>x]………..(9)(While规则)5)根据并置规则，有：

[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)y2>x]………………（10）7.4程序正确性验证–Hoare公理学方法6）[Q(x,y1)]Zy1[Q(x,z)](赋值公理)

得：[P(x,y)y2>x]Zy1[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);Zy1;