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

1、 山东大学山东大学 计算机科学与技术学院计算机科学与技术学院 嵌入式系统学科组嵌入式系统学科组 0 利用利用HOARE公理化方法证明程序部公理化方法证明程序部分正确性分正确性张兆朋张兆朋 山东大学山东大学 计算机科学与技术学院计算机科学与技术学院 嵌入式系统学科组嵌入式系统学科组 1 山东大学山东大学 计算机科学与技术学院计算机科学与技术学院 嵌入式系统学科组嵌入式系统学科组 2 1990年年IEEE计算机先驱奖计算机先驱奖1980年图灵奖年图灵奖英国牛津大学计算机科学家查尔斯英国牛津大学计算机科学家查尔斯.霍尔霍尔(Charles Antony Richard Hoare)发明发明Quick

2、sort算法、算法、CASE语句语句1963年实现了年实现了Algol语言语言1969年年1月，在月，在Comm. Of ACM上发表上发表“An Axiomatic basis for Computer Programming”,提出公提出公理语义学理语义学操作系统的操作系统的MonitorACM 在在1983年评出在近年评出在近25年在年在CACM上发表的上发表的25篇篇里程碑式的论文里程碑式的论文25篇，篇，2人人2篇，篇，Hoare是其一是其一 山东大学山东大学 计算机科学与技术学院计算机科学与技术学院 嵌入式系统学科组嵌入式系统学科组 3 BAAAn,21 山东大学山东大学 计算机科

3、学与技术学院计算机科学与技术学院 嵌入式系统学科组嵌入式系统学科组 4 山东大学山东大学 计算机科学与技术学院计算机科学与技术学院 嵌入式系统学科组嵌入式系统学科组 5 山东大学山东大学 计算机科学与技术学院计算机科学与技术学院 嵌入式系统学科组嵌入式系统学科组 6 山东大学山东大学 计算机科学与技术学院计算机科学与技术学院 嵌入式系统学科组嵌入式系统学科组 7 程序正确性证明程序正确性证明Hoare的公理化方法的公理化方法Hoare提出的公理和相应控制语句的证明规则。提出的公理和相应控制语句的证明规则。l 4. 并置规则并置规则P S1R,R S2 QP S1;S2 Q 山东大学山东大学 计

4、算机科学与技术学院计算机科学与技术学院 嵌入式系统学科组嵌入式系统学科组 8 山东大学山东大学 计算机科学与技术学院计算机科学与技术学院 嵌入式系统学科组嵌入式系统学科组 9 程序正确性验证程序正确性验证 Hoare公理学方法公理学方法证明过程证明过程 证明程序部分正确性的公理学方法就是依据以上的公理和推理规则证明程序部分正确性的公理学方法就是依据以上的公理和推理规则,一般一般有两种形式有两种形式:正向证明和反向证明正向证明和反向证明 正向正向“证明证明” : 从某些公理出发从某些公理出发, 使用规则使用规则, 直到最后获得结果直到最后获得结果.l 根据给出的不变式断言根据给出的不变式断言,建

5、立一些引理建立一些引理;l 根据引理和赋值公理根据引理和赋值公理,对程序中的每一个赋值语句对程序中的每一个赋值语句 Fi 导出相应的不导出相应的不变式语句变式语句Ri Fi Qi;l 再根据这些不变式语句和上述的推理规则逐步地组成越来越长的程再根据这些不变式语句和上述的推理规则逐步地组成越来越长的程序段序段,一直到推演出一直到推演出:P(x) F Q(x,z)为止为止. 山东大学山东大学 计算机科学与技术学院计算机科学与技术学院 嵌入式系统学科组嵌入式系统学科组 10 练习：练习：对任一给定的自然数对任一给定的自然数x，计算，计算 z = sqrt(x) 的程序流程的程序流程图如右。该程序的算

6、法基于：对于任意整数图如右。该程序的算法基于：对于任意整数n=0,有有 1+3+5+(2n+1)=(n+1)2P(x): x=0Q(x,y): z2 x=0(y1,y2,y3) (0,1,1);While ( y2=x ) do p(x,y): y12=x and y2=(y1+1)2 and y3=2*y1+1 (y1,y2,y3) (y1+1,y2+y3+2,y3+2);Z y1;Q(x,z) : z2=xx?y1+1,y2+y3+2,y3+2 y1,y2,y3y1 z结束P(x)AFBTDGCFq(x,y1,y2,y3) 山东大学山东大学 计算机科学与技术学院计算机科学与技术学院 嵌入式

7、系统学科组嵌入式系统学科组 12 7.4 程序正确性验证程序正确性验证 Hoare公理学方法公理学方法正向证明：正向证明：1) 首先建立引理：首先建立引理：引理引理1： P(x) P(x,0,1,1) .(1)引理引理2： P(x,y) y2xP(x,y1+1,y2+y3+2,y3+2) (2)引理引理3： P(x,y) y2 x Q(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)

8、 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) y2x (y1,y2,y3) (y1+1,y2+y3+2,y3+2) P(x,y) .(7) 山东大学山东大学 计算机科学与技术学院计算机科学与技术学院 嵌入式系统学科组嵌入式系统学科组 13 7.4 程序正确性验证程序正确性验证 Hoare公理学方法公理学方法4)取取I为为P(x,y), Q为为P(x,y) y2 x ，有：，有： PI, P(x,y) y2 x Q .(8) 得：得：P(x,

9、y) While ( y2x .(9) (While规则规则 )5) 根据并置规则，有：根据并置规则，有： x 0 (y1,y2,y3) (0,1,1); While ( y2x （10） 山东大学山东大学 计算机科学与技术学院计算机科学与技术学院 嵌入式系统学科组嵌入式系统学科组 14 7.4 程序正确性验证程序正确性验证 Hoare公理学方法公理学方法6）Q(x,y1) Z y1 Q(x,z) (赋值公理赋值公理) 得：得： P(x,y) y2 x 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+