形式化验证的非正式介绍培训课件.pptx

形式化验证的非正式介绍 南京大学计算机系 赵建华 1 为什么要形式化？ 自然语言天生具有二义性。原因： 上下文 生活/教育背景不同 故事：巴别塔 使用自然语言进行推导时不严谨 人很自然地会忽略“显然如此”的情况 即使是数学家的论文，其中也有论证。（但是结论通常是正确的） 解决办法之一：形式化 2 什么是形式化方法 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 3 逻辑 语法 说明了一个逻辑公式应该怎么写； 语义 指明了各个公式的含义； 推理系统 一组公理：最简单的、正确的公式模板； 一组推导规则：以一些公式作为前提，推导出一些其它公式。 4 逻辑的性质 Completeness 所有永真的公式都能证明； Soundness 所有可证明的公式都是永真的； Decidability 通过算法来判断一个公式是否永真 5 程序的形式化规约 当你使用一个程序时，你关心哪些性质？ 这些性质可能被无二义的描述出来吗？ 如果描述出来之后，我们有办法证明这个程序一定满足这个性质吗？ 6 Hoare三元式 Hoare三元式 {P} S {Q} S ：代码 P : (pre-condition，前置条件) Q : (post-condition，后置条件) P和Q是一阶逻辑公式 三元式指出了部分正确性 如果S从一个满足P的状态开始执行，且S 能够正常执行完毕，那么最后的状态满足Q。 7 程序的抽象语法 基本语句 赋值语句：v:=e skip语句 复合语句 顺序：S;S 选择：if p then S else S fi 循环：while p do S 8 公理一：赋值语句 {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} 9 公理：skip语句 skip语句不改变状态。 {P} skip {P} 10 pre, post规则 在证明了一个断言之后，我们可以弱化其后置条件，或者强化其前置条件。 P=P’，{P’} S {Q} {P} S {Q} {P} S {Q’}，Q’ = Q {P} S {Q} 11 顺序组合规则 在证明一个顺序组合语句的时候，我们可以先分别证明两个子语句的性质，然后将其合并得到整个组合语句的性质。 {P} S1 {Q}， {Q}S2{R} {P} S1;S2 {R} 12 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语句的含义我们可以知道结论成立。 13 while规则(部分正确性) {P∧p} S {P} {P} while p do S {P∧┒P} P被称为while语句的不变式。 在while语句的执行过程中，这个性质总是成立。 而while语句会执行到p不成立为止。 因此，当while语句退出循环时，状态必然满足P∧┒p。 这个性质不保证while语句会退出循环 14 例子（1） 整数除法的累减实现 y1=0; y2=x1; while y2x2 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 ∧ y2x2 15 例子（2） 可以按照如下方式证明： {x1=0 ∧ x20} y1=0; {x1=0 ∧ x20 ∧ y1=0} y2=x1; {x1=y1*x2+y2 ∧ y2=0} while y2=x2 do {x1=y1*x2+y2 ∧ y2=x2} y1:=y1+1; {x1=y