程序的公理化证明 赵建华 南京大学计算机系
简介 C.A.R. Hoare提出的公理系统 断言中包含了逻辑公式和代码 组合式证明 本证明系统基于某个一阶推理系统. 先证明程序的各个部分，然后把这些证明组合起来，得到更大代码的证明。 本证明系统基于某个一阶推理系统.
断言的形式 Hoare三元式 {P} S {Q} 三元式指出了一个部分正确性 S ：代码 P(pre-condition，前置条件) Q (post-condition，后置条件) P和Q是一阶逻辑公式 三元式指出了一个部分正确性 如果S从一个满足P的状态开始执行，且S 能够正常执行完毕，那么最后的状态满足Q。
程序的抽象语法 基本语句 复合语句 赋值语句：v:=e skip语句 顺序：S;S 选择：if p then S else S fi 循环：while p do S
公理：赋值语句 {Q[e/v]} v:=e {Q} 如果语句v:=e执行之前的状态满足 Q[e/v]，那么v:=e执行之后的状态满足Q。 Q[e/v]表示将公式Q中的v替换成为e后得到的公式。 例如：{x+1==10}x:=x+1{x==10}
公理：skip语句 skip语句不改变状态。 {P} skip {P}
pre,post规则 在证明了一个断言之后，我们可以弱化其后置条件，或者强化其前置条件。 P=>P’，{P’} S {Q} {P} S {Q’}，Q’ => Q
顺序组合规则 在证明一个顺序组合语句的时候，我们可以先分别证明两个子语句的性质，然后将其合并得到整个组合语句的性质。 {P} S1 {Q}， {Q}S2{R} {P} S1;S2 {R}
{P∧p} S1 {Q} ，{P∧┒p} S2 {Q} if-then-else规则 {P∧p} S1 {Q} ，{P∧┒p} S2 {Q} {P} if p then S1 else S2 {Q} if语句的语义是：如果p成立，则执行S1，否则执行S2。 前提条件表明 如果开始状态满足P∧p那么执行了S1 之后满足Q。 如果开始状态满足P∧┒p，那么执行S之后仍然满足Q。 如果开始状态满足P，那么它要么满足P∧p，要么满足P∧┒p。从if语句的含义我们可以知道结论成立。
while规则(部分正确性) {P∧p} S {P} {P}while p do S {φ∧┒P} P被称为while语句的不变式。
while规则(完全正确性) 如果能够找到一个函数f {f=f0} S {f<f0}, 那么循环必然终止 P∧p f>0 且对任意的常数f0， {f=f0} S {f<f0}, 那么循环必然终止 for(int i = 0; i<100; i++) …
例子（1） 整数除法的累减实现 要证明如下结论： y1=0; y2=x1; while y2>x2 do y1:=y1+1; end 要证明如下结论： 当x1>=0, x2>=0成立时，最终得到的y1是x1/x2的整数商部分，y2是x1/x2的余数部分即： Precondition: x1>=0 ∧ x2>=0 Postcondition：x1=y1*x2+y2 ∧ y2>=0 ∧ y2<x2
例子（2） 可以按照如下方式证明： {x1>=0 ∧ x2>0} y1=0; y2=x1; {x1=y1*x2+y2 ∧ y2>=0} while y2>=x2 do {x1=y1*x2+y2 ∧ y2>=x2} y1:=y1+1; {x1=y1*x2+y2-x2 ∧ y2>=x2} y2:=y2-x2 end {x1=y1*x2+y2 ∧ y2>=0 ∧ y2<x2}
练习 考虑辗转相除法求解GCD的算法的正确性证明 考虑图论中最短路径的Floyd算法的正确性。
Hoare Logic不能处理指针/数组 反例1： 反例2： {true} m[m[2]] := 3 {m[m[2]] == 3} {*p == *q} *p:=*p+1 {*p == *q+1} 当p和q指向同一个位置时，结果应该是*p==*q仍然成立。