形式化验证的非正式介绍 南京大学计算机系 赵建华

为什么要形式化？ 自然语言天生具有二义性。原因： 使用自然语言进行推导时不严谨 解决办法之一：形式化 上下文 生活/教育背景不同 故事：巴别塔 使用自然语言进行推导时不严谨 人很自然地会忽略“显然如此”的情况 即使是数学家的论文，其中也有论证。（但是结论通常是正确的） 解决办法之一：形式化

什么是形式化方法 In computer science, formal methods are a particular kind of mathematically based techniques for the specification, development and verification of software and hardware systems. logic calculi formal languages and automata theory program semantics type systems algebraic data types

逻辑 语法 语义 推理系统 说明了一个逻辑公式应该怎么写； 指明了各个公式的含义； 一组公理：最简单的、正确的公式模板； 一组推导规则：以一些公式作为前提，推导出一些其它公式。

逻辑的性质 Completeness Soundness Decidability 所有永真的公式都能证明； 所有可证明的公式都是永真的； 通过算法来判断一个公式是否永真

程序的形式化规约 当你使用一个程序时，你关心哪些性质？ 这些性质可能被无二义的描述出来吗？ 如果描述出来之后，我们有办法证明这个程序一定满足这个性质吗？

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} 前提条件表明 如果开始状态满足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} P被称为while语句的不变式。

例子（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}

主要的证明技术 最弱前置条件的计算 逻辑推导 其它自动的代码分析算法 最基本的原理：{Q[e/v]} v:=e {Q} 对于一个程序片段S，要证明{P} S {Q}，只需要证明P=>WP(S,Q) 逻辑推导 SMT Solver：Z3， 高阶逻辑工具：PVS，Coq，… 其它自动的代码分析算法

Hoare Logic需要扩充的地方 不能处理指针/数组引起的别名问题 不支持局部推导 不能直接表示变量的原值 {true} m[m[2]] := 3 {m[m[2]] == 3} 如果当原来m[2]=2时，赋值之后m[m[2]]的值是原来的m[3]，不一定等于3！ 不支持局部推导 在前面的证明中，对于赋值语句y1:=y1+1，我们必须证明： {x1=y1*x2+y2 ∧ y2>=x2} y1:=y1+1; {x1=y1*x2+y2-x2 ∧ y2>=x2} 不能直接表示变量的原值

谢谢