《第7章 程序验证》由会员分享，可在线阅读，更多相关《第7章 程序验证（32页珍藏版）》请在金锄头文库上搜索。
1、第7章程序验证 内容概述程序逻辑 描述和论证程序行为的逻辑Hoare逻辑Dijkstra最弱前条件演算从程序到定理验证条件生成从定理到证明定理证明器判定过程循环不变式的推断以GeorgeC Necula教授的讲稿为主来介绍 程序逻辑 Hoare逻辑良形公式 well formedformula 的形式为 P C Q C是程序片段需要介绍编程语言P和Q是断言需要介绍断言及推理规则 P C Q 称为程序规范需要介绍规范语言及推理规则Hoare逻辑也称为语言的一种公理语义 作为例子的核心编程语言 语法整数表达式E n x E E E E E E E E 布尔表达式B true false B By
2、y z Hoare逻辑 断言语言用来描述程序变量满足的性质 如x 5 x y 30通常 断言P Q的语法同编程语言布尔表达式的语法有些区别 如可以出现量词Hoare逻辑的良形公式 P C Q C是一段程序 P和Q分别是C的前条件和后条件例如 x 5 x x 1 x 6 Hoare逻辑 Hoare逻辑良形公式 P C Q 的解释部分正确性在满足P的任何状态下执行C 若C终止则结果状态一定满足Q 记作 par P C Q 完全正确性在满足P的任何状态下执行C 则C一定终止并且结果状态一定满足Q 记作 tot P C Q 通常建议用部分正确性证明 终止性证明来得到完全正确性证明 Hoare逻辑 例1
3、Succ 例2Fac1 x 0 a x 1 y 1 if a 1 0 z 0 y 1 while z x else z z 1 y a y y z y x 1 y x Hoare逻辑 例2Fac1 例3Fac2 x 0 x0是辅助的逻辑变量y 1 x 0 x x0 z 0 y 1 while z x while x 0 z z 1 y y x y y z x x 1 y x y x0 Hoare逻辑 部分正确性的证明规则赋值公理赋值公理的实例 2 2 x 2 x 2 2 4 x 2 x 4 2 y x 2 x y 2 0 x 2 x 0 x 1 5 y x x 1 x 5 y x 1 0 y
4、0 x x 1 x 0 y 0 Hoare逻辑 部分正确性的证明规则赋值公理复合规则条件规则循环规则 Hoare逻辑 部分正确性的证明规则推论规则 ARP P表示P P在谓词逻辑的自然演绎演算中可以证明 Hoare逻辑 n 0functionmult m n 0 m 0 0 n x 0 x m 0 0 n y 0 x m y y n whiley ndo x m m y 1 y 1 n x x m x m y 1 y 1 n y y 1 x m y y n x m n 一个简单的例子 最弱前条件演算 Dijkstra的思路为了验证 P C Q 找出所有使得 P C Q 的断言P 称为Pre C
5、 Q 验证存在P Pre C Q thatP P 这些断言形成一个格变成计算WP C Q 并且证明P WP C Q 最弱前条件演算 断言形成一个格WP C Q lub Pre C Q 按上面的式子计算WP C Q 有时是困难的1 lub P1 P2 P1 P22 lubPS P PSP3 但是当集合PS无限时怎么办 最弱前条件演算 断言形成一个格WP C Q lub Pre C Q 按上面的式子计算WP C Q 有时是困难的1 lub P1 P2 P1 P22 lubPS P PSP3 但是当集合PS无限时怎么办 即使得到了WP C Q 检查蕴涵P WP C Q 也可能是困难的 最弱前条件演算
6、 演算规则 和Hoare逻辑规则对比 WP x E Q Q E x WP C1 C2 Q WP C1 WP C2 Q WP ifB C1 else C2 Q B WP C1 Q B WP C2 Q 最弱前条件演算 演算规则对于循环语句怎么办 定义一族WPWPk whileB C Q 循环的执行终止于不多于k次的迭代 其终止状态满足Q 的最弱前条件 WP0 B QWP1 B WP C WP0 B Q WP whileB C Q k 0WPk lub WPk k 0 最弱前条件演算 演算规则计算非常困难能否找到容易一些并且够用的办法WPk whileB C Q 循环的执行终止于不多于k次的迭代 其
7、终止状态满足Q 的最弱前条件 WP0 B QWP1 B WP C WP0 B Q WP whileB C Q k 0WPk lub WPk k 0 验证条件生成 验证条件回想一下我们想达到的目的 验证条件生成 验证条件回想一下我们想达到的目的我们构造一个验证条件VC C Q 1 循环需要有循环不变式标注2 VC要强于WP3 但仍然要弱于P P VC C Q WP C Q 验证条件生成 验证条件循环不变式很难写出 考虑源于QuickSort的代码intpartition int a intL0 intH0 intpivot intL L0 H H0 while Lpivot H if L H s
8、wapa L anda H returnL 仅考虑内存安全 外循环的不变式是什么 循环不变式的自动生成是尚未解决的问题 验证条件生成 验证条件生成VC的计算方式类似于WP的计算只有while语句例外VC whileB C Q I I B VC C I I B Q 循环不变式I由外部提供 验证条件生成 functionmult m n x 0 y 0 whiley ndo x x m y y 1 以这个函数为例 解释验证条件生成 验证条件生成 n 0 前条件functionmult m n x 0 y 0 whiley ndo x x m y y 1 x m n 后条件 由程序设计者提供 由程序
9、设计者提供 验证条件生成 n 0functionmult m n x 0 y 0 whiley ndo x m y y n 循环不变式x x m y y 1 x m n 也由程序设计者提供 验证条件生成 n 0functionmult m n x 0 y 0 whiley ndo x m y y n x x m y y 1 x m y y n y n x m n x m n 第一个验证条件 由验证条件生成器生成 验证条件生成 n 0functionmult m n x 0 y 0 whiley ndo x m y y n x x m x m y 1 y 1 n y y 1 在语句序列中的断言
10、x m y y n y n x m n x m n 由最弱前条件演算插入 验证条件生成 n 0functionmult m n x 0 y 0 whiley ndo x m y y n x m m y 1 y 1 n x x m x m y 1 y 1 n y y 1 x m y y n y n x m n x m n 验证条件生成 n 0functionmult m n x 0 y 0 x m y y n y n x m m y 1 y 1 n whiley ndo x m y y n x m m y 1 y 1 n x x m x m y 1 y 1 n y y 1 x m y y n y
11、 n x m n x m n 第2个验证条件 验证条件生成 n 0functionmult m n x 0 x m 0 0 n y 0 x m y y n y n x m m y 1 y 1 n whiley ndo x m y y n x m m y 1 y 1 n x x m x m y 1 y 1 n y y 1 x m y y n y n x m n x m n 验证条件生成 n 0functionmult m n 0 m 0 0 n x 0 x m 0 0 n y 0 x m y y n y n x m m y 1 y 1 n whiley ndo x m y y n x m m y
12、 1 y 1 n x x m x m y 1 y 1 n y y 1 x m y y n y n x m n x m n 验证条件生成 n 0functionmult m n n 0 0 m 0 0 n 0 m 0 0 n x 0 x m 0 0 n y 0 x m y y n y n x m m y 1 y 1 n whiley ndo x m y y n x m m y 1 y 1 n x x m x m y 1 y 1 n y y 1 x m y y n y n x m n x m n 第3个验证条件 验证条件生成 n 0functionmult m n n 0 0 m 0 0 n x 0 y 0 x m y y n y n x m m y 1 y 1 n whiley ndo x m y y n x x m y y 1 x m y y n y n x m n x m n 这三个验证条件需要证明
