《教学课件第7章程序验证》由会员分享，可在线阅读，更多相关《教学课件第7章程序验证（32页珍藏版）》请在金锄头文库上搜索。
1、第第7章章 程序验证程序验证内容概述内容概述程序逻辑：描述和论证程序行为的逻辑程序逻辑：描述和论证程序行为的逻辑Hoare逻辑逻辑Dijkstra最弱前条件演算最弱前条件演算从程序到定理从程序到定理验证条件生成验证条件生成从定理到证明从定理到证明定理证明器定理证明器判定过程判定过程循环不变式的推断循环不变式的推断以以George C. Necula教授的讲稿为主来介绍教授的讲稿为主来介绍程程 序序 逻逻 辑辑Hoare逻辑逻辑良形公式良形公式（well-formed formula）的形式为的形式为 P C Q C是程序片段是程序片段需要介需要介绍编程程语言言P 和和Q是断言是断言需要介需要介
2、绍断言及推理断言及推理规则 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 |while B C 例子例子y = 1; z = 0; while (z != x)
3、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 = x0 z = 0; y = 1; while ( z != x ) while ( x != 0 ) z
4、 = 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 Q Hoare逻辑逻辑部分正确性的证明规则部分正确性的证明规则赋值公理公理复合复合规则条件条件规则循循环规则 QE/
5、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 = 0function mult(m, n) (0 = m 0) (0 = n) x = 0 ; (x = m 0) (0 = n) y = 0 ; (x = m
6、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, Q)验证存在验证存在P Pre(C, Q) that P P 这些断言形成一个格这些断言形成一个格变成计算变成计算WP(C, Q)并且证明并且证明P WP
7、(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无限时怎么办？无限时怎么办？最弱前条件演算最弱前条件演算断言形成一个格断言形成一个格 WP(C, Q) = lub(Pre(C, Q)按上面的式子计算按上面的式子计算WP(C, Q)有时是困难的有时是困难的1、lub P1,
8、 P2 = P1 P22、lub PS = P PS P3、但是当集合、但是当集合PS无限时怎么办？无限时怎么办？即使得到了即使得到了WP(C, Q)，检查蕴涵，检查蕴涵P WP(C, Q)也也可能是困难的可能是困难的最弱前条件演算最弱前条件演算演算规则（和演算规则（和Hoare逻辑规则对比）逻辑规则对比）WP(x = E, Q) = QE/xWP(C1;C2 , Q) = WP (C1, WP(C2, Q)WP(if 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
9、C1 Q P B C2 Q P if B C1 else C2 Q 最弱前条件演算最弱前条件演算演算规则演算规则对于循环语句怎么办？对于循环语句怎么办？ 定义一族定义一族WPWPk(while B C , Q) = “循环的执行终止于不多循环的执行终止于不多于于k次的迭代，其终止状态满足次的迭代，其终止状态满足Q”的最弱前条件：的最弱前条件：WP0 = B QWP1 = B WP(C, WP0) B Q. . .WP(while B C, Q) = k 0WPk = lubWPk | k 0 I B C I I while B C Q 最弱前条件演算最弱前条件演算演算规则演算规则计算非常困难计
10、算非常困难能否找到容易一些并且够用的办法能否找到容易一些并且够用的办法WPk(while B C , Q) = “循环的执行终止于不多循环的执行终止于不多于于k次的迭代，其终止状态满足次的迭代，其终止状态满足Q”的最弱前条件：的最弱前条件：WP0 = B QWP1 = B WP(C, WP0) B Q. . .WP(while B C, Q) = k 0WPk = lubWPk | k 0验证条件生成验证条件生成验证条件验证条件回想一下我们想达到的目的回想一下我们想达到的目的falsetrue强强弱弱Pre(C, Q)P最弱前条件最弱前条件WP(C, Q)验证条件生成验证条件生成验证条件验证条
11、件回想一下我们想达到的目的回想一下我们想达到的目的我们构造一个验证条件我们构造一个验证条件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)验证条件生成验证条件生成验证条件验证条件循环不变式很难写出循环不变式很难写出, 考虑源于考虑源于QuickSort的代码的代码int partition(int *a, int L0, int H0, int pivot) in
12、t L = L0, H = H0; while(L H) while(aL pivot) H -; if(L H) swap aL and aH return L / 仅考虑内存安全，外循环的不变式是什么？仅考虑内存安全，外循环的不变式是什么？循环不变式的自动生成是尚未解决的问题循环不变式的自动生成是尚未解决的问题验证条件生成验证条件生成验证条件生成验证条件生成VC的计算方式类似于的计算方式类似于WP的计算的计算只有只有while语句例外语句例外VC(while B C , Q ) = I ( I B VC(C, I) ) ( I B Q )循环不变式循环不变式 I 由外部提供由外部提供 I
13、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 ; 以这个函数为以这个函数为例，解释验证例，解释验证条件生成条件生成验证条件生成验证条件生成n 0/ 前条件前条件function mult(m, n) x = 0 ; y = 0 ;while y n do x = x + m ;y = y + 1 ; x = m n/ 后条件后
14、条件由程序设由程序设计者提供计者提供由程序设由程序设计者提供计者提供验证条件生成验证条件生成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 (x = m y) (y n) x = x + m ;y = y + 1 ; (x = m y) (y n) (y n) (x
15、= 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由最弱前条由最弱前条件演算插入件演算插入验证条件生成验证条件生成n 0function mult(m, n) x = 0 ; y =
16、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)while y n do (x = m y) (y n) (x+m = m (y+1) (y+1) n) x = x + m ;(
17、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+1) (y+1) n) x = x + m ;(x = m (y+1) (y+1) n) y = y + 1 ; (x = m
18、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验证条件生成
19、验证条件生成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 + 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 0function mult(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)while y n do (x = m y) (y n) x = x + m ;y = y + 1 ; (x = m y) (y n) (y n) (x = m n) x = m n这三个验证条这三个验证条件需要证明件需要证明
