第7章程序验证(编辑修改稿)

第7章程序验证(编辑修改稿)内容摘要：

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 } 最弱前条件演算 • 演算规则 – 对于循环语句怎么办。 – 定义一族 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) 循环需要有循环不变式标注 VC要强于 WP 但仍然要弱于 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 ) – 循环。