P - 南京大学计算机科学与技术系

Report
形式化验证的非正式介绍
南京大学计算机系
赵建华
为什么要形式化?
• 自然语言天生具有二义性。原因:
– 上下文
– 生活/教育背景不同
– 故事:巴别塔
• 使用自然语言进行推导时不严谨
– 人很自然地会忽略“显然如此”的情况
– 即使是数学家的论文,其中也有论证。(但是
结论通常是正确的)
• 解决办法之一:形式化
什么是形式化方法
• 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}
{P} S {Q’},Q’ => Q
{P} S {Q}
顺序组合规则
• 在证明一个顺序组合语句的时候,我们可
以先分别证明两个子语句的性质,然后将
其合并得到整个组合语句的性质。
{P} S1 {Q}, {Q}S2{R}
{P} S1;S2 {R}
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语句的不变式。
– 在while语句的执行过程中,这个性质总是成立。
• 而while语句会执行到p不成立为止。
– 因此,当while语句退出循环时,状态必然满足
P∧┒p。
• 这个性质不保证while语句会退出循环
例子(1)
• 整数除法的累减实现
y1=0;
y2=x1;
while y2>x2 do
y1:=y1+1;
y2:=y2-x2
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;
{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
{x1=y1*x2+y2 ∧ y2>=0}
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}
• 不能直接表示变量的原值

similar documents