《【教学课件】第7章程序验证.ppt》由会员分享，可在线阅读，更多相关《【教学课件】第7章程序验证.ppt（32页珍藏版）》请在三一办公上搜索。
1、第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|f
2、alse|!B|B y=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 通常建议用部分正确性证明终止性证明来得到完全正确性证明
3、,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逻辑,部分正确性的证明规则赋值公理赋值公理的实例 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
4、 x=x+1 x+5=y x+1 0 y 0 x=x+1 x 0 y 0,Hoare逻辑,部分正确性的证明规则赋值公理复合规则条件规则循环规则,Hoare逻辑,部分正确性的证明规则推论规则AR P P 表示P P在谓词逻辑的自然演绎演算中可以证明,Hoare逻辑,n=0function mult(m,n)(0=m0)(0=n)x=0;(x=m0)(0=n)y=0;(x=my)(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=my)(y=n)x=m n,/一个简单的例子,最弱前条件演算,Dijkstra的思路为
5、了验证 P C Q，找出所有使得 P C Q 的断言P，称为Pre(C,Q)验证存在P Pre(C,Q)that P P这些断言形成一个格变成计算WP(C,Q)并且证明P WP(C,Q),最弱前条件演算,断言形成一个格 WP(C,Q)=lub(Pre(C,Q)按上面的式子计算WP(C,Q)有时是困难的1、lub P1,P2=P1 P22、lub PS=PPS P3、但是当集合PS无限时怎么办？,最弱前条件演算,断言形成一个格 WP(C,Q)=lub(Pre(C,Q)按上面的式子计算WP(C,Q)有时是困难的1、lub P1,P2=P1 P22、lub PS=PPS P3、但是当集合PS无限时怎
6、么办？即使得到了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),最弱前条件演算,演算规则对于循环语句怎么办？定义一族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,最弱前条件演算,演算规则计
7、算非常困难能否找到容易一些并且够用的办法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,验证条件生成,验证条件回想一下我们想达到的目的,验证条件生成,验证条件回想一下我们想达到的目的我们构造一个验证条件VC(C,Q)1、循环需要有循环不变式标注2、VC要强于WP3、但仍然要弱于P，P VC(C,Q)WP(C,Q),验证条件生成,验证条件循环不变式很难写出,考虑源于QuickSort的代码int partition(int*
8、a,int L0,int H0,int pivot)int L=L0,H=H0;while(L 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 由外部提供,验证条件生成,function mult(m,n)x=0;y=0;while y n do x=x+m;y=y+1;,以这个函数为例，解释验证条件生成,验证条件生成,n
9、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=my)(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=my)(y n)x=x+m;y=y+1;(x=my)(y n)(y n)(x=mn)x=m n/第一个验证条件,由验证条件生成器生成,验证条件生
10、成,n 0function mult(m,n)x=0;y=0;while y n do(x=my)(y n)x=x+m;(x=m(y+1)(y+1)n)y=y+1;/在语句序列中的断言(x=my)(y n)(y n)(x=mn)x=m n,由最弱前条件演算插入,验证条件生成,n 0function mult(m,n)x=0;y=0;while y n do(x=my)(y n)(x+m=m(y+1)(y+1)n)x=x+m;(x=m(y+1)(y+1)n)y=y+1;(x=my)(y n)(y n)(x=mn)x=m n,验证条件生成,n 0function mult(m,n)x=0;y=0;
11、(x=my)(y n)(y n)(x+m=m(y+1)(y+1)n)while y n do(x=my)(y n)(x+m=m(y+1)(y+1)n)x=x+m;(x=m(y+1)(y+1)n)y=y+1;(x=my)(y n)(y n)(x=mn)x=m n,第2个验证条件,验证条件生成,n 0function mult(m,n)x=0;(x=m0)(0 n)y=0;(x=my)(y n)(y n)(x+m=m(y+1)(y+1)n)while y n do(x=my)(y n)(x+m=m(y+1)(y+1)n)x=x+m;(x=m(y+1)(y+1)n)y=y+1;(x=my)(y n)
12、(y n)(x=mn)x=m n,验证条件生成,n 0function mult(m,n)(0=m0)(0 n)x=0;(x=m0)(0 n)y=0;(x=my)(y n)(y n)(x+m=m(y+1)(y+1)n)while y n do(x=my)(y n)(x+m=m(y+1)(y+1)n)x=x+m;(x=m(y+1)(y+1)n)y=y+1;(x=my)(y n)(y n)(x=mn)x=m n,验证条件生成,n 0function mult(m,n)(n 0)(0=m0)(0 n)(0=m0)(0 n)x=0;(x=m0)(0 n)y=0;(x=my)(y n)(y n)(x+m=m(y+1)(y+1)n)while y n do(x=my)(y n)(x+m=m(y+1)(y+1)n)x=x+m;(x=m(y+1)(y+1)n)y=y+1;(x=my)(y n)(y n)(x=mn)x=m n,第3个验证条件,验证条件生成,n 0function mult(m,n)(n 0)(0=m0)(0 n)x=0;y=0;(x=my)(y n)(y n)(x+m=m(y+1)(y+1)n)while y n do(x=my)(y n)x=x+m;y=y+1;(x=my)(y n)(y n)(x=mn)x=m n,这三个验证条件需要证明,
