第7章程序验证

1、第第7章章 程序验证程序验证内容概述内容概述 程序逻辑：描述和论证程序行为的逻辑程序逻辑：描述和论证程序行为的逻辑 Hoare逻辑逻辑 Dijkstra最弱前条件演算最弱前条件演算 从程序到定理从程序到定理 验证条件生成验证条件生成 从定理到证明从定理到证明 定理证明器定理证明器 判定过程判定过程 循环不变式的推断循环不变式的推断 以以George C. Necula教授的讲稿为主来介绍教授的讲稿为主来介绍程程 序序 逻逻 辑辑 Hoare逻辑逻辑 良形公式良形公式（well-formed formula）的形式为的形式为 P C Q C是程序片段是程序片段需要介绍编程语言需要介绍编程语言 P

2、 和和Q是断言是断言需要介绍断言及推理规则需要介绍断言及推理规则 P C Q 称为程序规范称为程序规范需要介绍规范语言及推理规则需要介绍规范语言及推理规则 Hoare逻辑也称为语言的一种公理语义逻辑也称为语言的一种公理语义作为例子的核心编程语言作为例子的核心编程语言 语法语法 整数表达式整数表达式E := n | x | E | E + E | E E | E E | ( E ) 布尔表达式布尔表达式B := true | false | !B | B & B | B | B | E E | ( B ) 命令命令C := x = E | C ; C | if B C else C |w

3、hile B C 例子例子y = 1; z = 0; while (z != x) z = z +1; y = y z Hoare逻辑逻辑 断言语言断言语言 用来描述程序变量满足的性质，如用来描述程序变量满足的性质，如x=5, x+y = 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逻辑逻辑 例例2 Fac1 例例3 Fac2 x = 0 x0是辅助的逻辑变量是辅助的逻辑变量 y = 1; x = 0 x =

4、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 0 x = x + 1 x 0 y 0 QE/x x = E

5、 Q Hoare逻辑逻辑 部分正确性的证明规则部分正确性的证明规则 赋值公理赋值公理 复合规则复合规则 条件规则条件规则 循环规则循环规则 QE/x x = E Q P C1 R R C2 Q P C1; C2 Q P B C1 Q P B C2 Q P if B C1 else C2 Q I B C I I while B C I B Hoare逻辑逻辑 部分正确性的证明规则部分正确性的证明规则 推论规则推论规则AR P P 表示表示P P在谓词逻辑的自然演绎演在谓词逻辑的自然演绎演算中可以证明算中可以证明 AR P P P C Q AR Q Q P C Q Hoare逻辑逻辑n = 0fu

6、nction mult(m, n) (0 = m 0) (0 = n) x = 0 ; (x = m 0) (0 = n) y = 0 ; (x = m y) (y = n) while y n do (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

7、, Q) 验证存在验证存在P Pre(C, Q) that P P 这些断言形成一个格这些断言形成一个格 变成计算变成计算WP(C, Q)并且证明并且证明P WP(C, Q)falsetrue强强弱弱Pre(C, Q)最弱前条件最弱前条件WP(C, Q)P最弱前条件演算最弱前条件演算 断言形成一个格断言形成一个格 WP(C, Q) = lub(Pre(C, Q) 按上面的式子计算按上面的式子计算WP(C, Q)有时是困难的有时是困难的1、lub P1, P2 = P1 P22、lub PS = P PS P3、但是当集合、但是当集合PS无限时怎么办？无限时怎么办？最弱前条件演算最弱前条件演算

8、断言形成一个格断言形成一个格 WP(C, Q) = lub(Pre(C, Q) 按上面的式子计算按上面的式子计算WP(C, Q)有时是困难的有时是困难的1、lub P1, P2 = P1 P22、lub PS = P PS P3、但是当集合、但是当集合PS无限时怎么办？无限时怎么办？ 即使得到了即使得到了WP(C, Q)，检查蕴涵，检查蕴涵P WP(C, Q)也可能是困难的也可能是困难的最弱前条件演算最弱前条件演算 演算规则（和演算规则（和Hoare逻辑规则对比）逻辑规则对比） WP(x = E, Q) = QE/x WP(C1;C2 , Q) = WP (C1, WP(C2, Q) WP(i

9、f B C1 else C2, Q) = (B WP(C1, Q) ( B WP(C2, Q) QE/x x = E Q P C1 R R C2 Q P C1; C2 Q P B C1 Q P B C2 Q P if B C1 else C2 Q 最弱前条件演算最弱前条件演算 演算规则演算规则 对于循环语句怎么办？对于循环语句怎么办？ 定义一族定义一族WP WPk(while B C , Q) = “循环的执行终止于不循环的执行终止于不多于多于k次的迭代，其终止状态满足次的迭代，其终止状态满足Q”的最弱前的最弱前条件：条件： WP0 = B Q WP1 = B WP(C, WP0) B Q.

10、. . WP(while B C, Q) = k 0WPk = lubWPk | k 0 I B C I I while B C Q 最弱前条件演算最弱前条件演算 演算规则演算规则 计算非常困难计算非常困难 能否找到容易一些并且够用的办法能否找到容易一些并且够用的办法 WPk(while B C , Q) = “循环的执行终止于不循环的执行终止于不多于多于k次的迭代，其终止状态满足次的迭代，其终止状态满足Q”的最弱前的最弱前条件：条件： WP0 = B Q WP1 = B WP(C, WP0) B Q. . . WP(while B C, Q) = k 0WPk = lubWPk | k 0验

11、证条件生成验证条件生成 验证条件验证条件 回想一下我们想达到的目的回想一下我们想达到的目的falsetrue强强弱弱Pre(C, Q)P最弱前条件最弱前条件WP(C, Q)验证条件生成验证条件生成 验证条件验证条件 回想一下我们想达到的目的回想一下我们想达到的目的 我们构造一个验证条件我们构造一个验证条件VC(C, Q)1、循环需要有循环不变式标注、循环需要有循环不变式标注2、VC要强于要强于WP3、但仍然要弱于、但仍然要弱于P， P VC(C, Q) WP(C, Q)falsetrue强强弱弱Pre(C, Q)最弱前条件最弱前条件WP(C, Q)P验证条件验证条件VC(C, Q)验证条件生成

12、验证条件生成 验证条件验证条件 循环不变式很难写出循环不变式很难写出, 考虑源于考虑源于QuickSort的代码的代码int partition(int *a, int L0, int H0, int pivot) int L = L0, H = H0; while(L H) while(aL pivot) H -; if(L H) swap aL and aH return L / 仅考虑内存安全，外循环的不变式是什么？仅考虑内存安全，外循环的不变式是什么？ 循环不变式的自动生成是尚未解决的问题循环不变式的自动生成是尚未解决的问题验证条件生成验证条件生成 验证条件生成验证条件生成 VC的计算

13、方式类似于的计算方式类似于WP的计算的计算 只有只有while语句例外语句例外VC(while B C , Q ) = I ( I B VC(C, I) ) ( I B Q ) 循环不变式循环不变式 I 由外部提供由外部提供 I B C I I while B C Q I 在循环在循环入口成立入口成立I 在循环任意在循环任意次迭代都保持次迭代都保持Q 在循环终在循环终止时成立止时成立验证条件生成验证条件生成function mult(m, n) x = 0 ; y = 0 ;while y n do x = x + m ;y = y + 1 ; 以这个函数为以这个函数为例，解释验证例，解释验证

14、条件生成条件生成验证条件生成验证条件生成n 0/ 前条件前条件function mult(m, n) x = 0 ; y = 0 ;while y n do x = x + m ;y = y + 1 ; x = m n/ 后条件后条件验证条件生成验证条件生成n 0function mult(m, n) x = 0 ; y = 0 ;while y n do (x = m y) (y n) / 循环不变式循环不变式x = x + m ;y = y + 1 ; x = m n验证条件生成验证条件生成n 0function mult(m, n) x = 0 ; y = 0 ;while y n do

15、 (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 0function mult(m, n) x = 0 ; y = 0 ;while y n do (x = m y) (y 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由最

16、弱前条由最弱前条件演算插入件演算插入验证条件生成验证条件生成n 0function mult(m, n) x = 0 ; y = 0 ;while y n do (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 0function mult(m, n) x = 0 ; y = 0 ;(x = m y) (y n) (y n) (x+m = m (y+1) (y+1) n)

17、while y n do (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第第2个验证条件个验证条件验证条件生成验证条件生成n 0function mult(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)while y n do (x = m y) (y n) (x+m = m (y

18、+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 0function mult(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)while y n do (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 0function mult(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)while y n do (x = m y) (y n) (x+m = m (y+1) (y+1) n) x = x +