第7章 程序验证 内容概述 程序逻辑：描述和论证程序行为的逻辑 从程序到定理 从定理到证明 循环不变式的推断 第7章 程序验证 内容概述 程序逻辑：描述和论证程序行为的逻辑 Hoare逻辑 Dijkstra最弱前条件演算 从程序到定理 验证条件生成 从定理到证明 定理证明器 判定过程 循环不变式的推断 以George C. Necula教授的讲稿为主来介绍

程 序 逻 辑 Hoare逻辑 良形公式（well-formed formula）的形式为 { 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 | 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) { z = z +1; y = y  z }

Hoare逻辑 断言语言 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 Succ  例2 Fac1 {  } { 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逻辑  例2 Fac1  例3 Fac2 { 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逻辑 部分正确性的证明规则 赋值公理 { Q[E/x] } x = E { Q } 赋值公理的实例 { 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 } { Q[E/x] } x = E { Q }

Hoare逻辑 部分正确性的证明规则 赋值公理 { Q[E/x] } x = E { Q } 复合规则 条件规则 循环规则 { Q[E/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}

AR P P { P } C { Q } AR Q  Q Hoare逻辑 部分正确性的证明规则 推论规则 AR P P 表示P P在谓词逻辑的自然演绎演 算中可以证明 AR P P { P } C { Q } AR Q  Q { P } C { Q }

Hoare逻辑 //一个简单的例子 n >= 0 function mult(m, 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  n

最弱前条件演算 Dijkstra的思路 为了验证 { P } C { Q }，找出所有使得 { P } C { Q }的断言P，称为Pre(C, Q) 验证存在P Pre(C, Q) that P  P 这些断言形成一个格 变成计算WP(C, Q)并且证明P  WP(C, Q) false true  强 弱 Pre(C, Q) 最弱前条件WP(C, Q) P

最弱前条件演算 断言形成一个格 WP(C, Q) = lub(Pre(C, Q)) 按上面的式子计算WP(C, Q)有时是困难的 1、lub {P1, P2} = P1  P2 2、lub PS = PPS P 3、但是当集合PS无限时怎么办？

最弱前条件演算 断言形成一个格 WP(C, Q) = lub(Pre(C, Q)) 按上面的式子计算WP(C, Q)有时是困难的 1、lub {P1, P2} = P1  P2 2、lub PS = PPS P 3、但是当集合PS无限时怎么办？ 即使得到了WP(C, Q)，检查蕴涵P  WP(C, Q)也可能是困难的

最弱前条件演算 演算规则（和Hoare逻辑规则对比） WP(x = E, Q) = Q[E/x] WP(C1;C2 , Q) = WP (C1, WP(C2, Q)) WP(if B {C1} else {C2}, Q) = (B  WP(C1, Q))  (B  WP(C2, Q)) { Q[E/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 } 定义一族WP WPk(while B { C }, Q) = “循环的执行终止于不多于k次的迭代，其终止状态满足Q”的最弱前条件： WP0 =  B  Q WP1 = B  WP(C, WP0)   B  Q . . . WP(while B {C}, Q) = k 0WPk = lub{WPk | 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 = lub{WPk | k  0}

验证条件生成 验证条件 回想一下我们想达到的目的 false true  强 弱 Pre(C, Q) P 最弱前条件WP(C, Q)

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

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

验证条件生成 验证条件生成 VC的计算方式类似于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 ; } 以这个函数为例，解释验证条件生成

验证条件生成 由程序设计者提供 由程序设计者提供 n  0 // 前条件 function mult(m, n){ x = 0 ; y = 0 ; while y < n do { x = x + m ; y = y + 1 ; } } x = m  n // 后条件 由程序设计者提供 由程序设计者提供

验证条件生成 也由程序设计者提供 n  0 function 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  0 function 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 = mn) } x = m  n // 第一个验证条件 由验证条件生成器生成

验证条件生成 由最弱前条件演算插入 n  0 function 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  0 function 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

验证条件生成 第2个验证条件 n  0 function 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 ; (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  0 function 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y)  (y  n))  (y < n)  (x = mn) } x = m  n

验证条件生成 n  0 function 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  0 function 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  0 function 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 这三个验证条件需要证明