程序验证(十):演绎验证(上)

Tattoo

发布日期: 2020-07-02 19:18:16 浏览量: 19
评分:
star star star star star star star star star star
*转载请注明来自write-bug.com

版权声明:本文为CSDN博主「swy_swy_swy」的原创文章,遵循CC 4.0 BY-SA版权协议,转载请附上原文出处链接及本声明。
原文链接:https://blog.csdn.net/swy_swy_swy/article/details/106751208

一、基础路径(Basic Approach)

给定一个程序cc,由以下specification注解:

{P}c{Q}\{P\}c\{Q\}

为了证明这个三元组,我们构造一个验证条件(verification condition, VC)的集合:

  • 每个VC都是某个理论的一阶公式

  • 如果所有的VC都是永真的,那么{P}c{Q}\lbrace P \rbrace c \lbrace Q \rbrace就是永真的

二、谓词转换器

给定一个断言QQ和一个程序cc,一个谓词转换器(predicate transformer)是一个函数,输出另一个断言。

最弱前置条件(weakest precondition)谓词转换器产生一个wp(c,Q)wp(c,Q),使得:

  • 对于[wp(c,Q)]c[Q][wp(c,Q)]c[Q]是永真的,且

  • 对于任何满足[P]c[Q][P]c[Q]PPPwp(c,Q)P\Rightarrow wp(c,Q),也就是说,wp(c,Q)wp(c,Q)是这种断言中最弱的

广义最弱前置条件(weakest liberal precondition)谓词转换器产生一个wlp(c,Q)wlp(c,Q),使得:

  • 对于wlp(c,Q)cQ{wlp(c,Q)}c{Q}是永真的,且

  • 对于wlp(c,Q)wlp(c,Q)是这种断言中最弱的

wlpwlp为我们提供了一种逆向的思路,这也符合我们的直觉。

三、wlp的定义

我们用霍尔三元组来定义wlpwlp

wlp(y:=x+1,(x.x<zx<y)x+1y)=?wlp(y:=x+1, (\forall x.x < z \to x < y) \to x+1\le y)=?

注意,答案并不是:

(x.x<zx<x+1)x+1x+1(\forall x.x < z\to x < x+1) \to x+1 \le x+1

因为当我们用x+1x+1替换yy以处理:

(x.x<zx<y)(\forall x.x < z\to x < y)

时,变量xx是被捕获的(captured)

3.1 捕获避免代入(capture-avoiding substitution)

当我们扩展P[a/x]P[a/x]时,我们需要:

  • 只代入xx的自由形式(free occurence)

  • aa中不自由的变量重命名以避免捕获

3.2 数组赋值规则

数组赋值的霍尔规则可以表示为:

AsgnArr {Q[xa1a2/x]}x[a1]:=a2{Q}AsgnArr~\frac{}{\{Q[x\langle a_1\triangleleft a_2\rangle /x]\}x[a_1]:=a_2\{Q\}}

相应的转换器即为:

wlp(x[a1]:=a2,Q)=Q[xa1a2/x]wlp (x[a_1]:=a_2,Q)=Q[x\langle a_1\triangleleft a_2\rangle /x]

举例:计算

wlp(b[i]:=5,b[i]=5)wlp(b[i]:=5,b[i]=5)

wlp(b[i]:=5,b[i]=5)=(b5[i]=5)=(5=5)=truewlp(b[i]:=5,b[i]=5)=(b\langle\triangleleft 5\rangle [i]=5)=(5=5)=true

计算

wlp(b[n]:=x,i.1i<nb[i]b[i+1])wlp(b[n]:=x,\forall i.1\le i < n\to b[i]\le b[i+1])

进行代入

wlp(b[n]:=x,i.1i<nb[i]b[i+1])=i.1i<n(bx)[i](bnx)[i+1]=(bnx)[n1](bnx)[n]i.1i<n1(bnx)[i](bnx)[i+1]wlp(b[n]:=x,\forall i.1\le i < n\to b[i]\le b[i+1])=\forall i.1\le i < n\to (b\langle\triangleleft x\rangle)[i]\le (b\langle n\triangleleft x\rangle)[i+1]=(b\langle n\triangleleft x\rangle)[n-1]\le (b\langle n\triangleleft x\rangle)[n]\wedge \forall i.1\le i < n-1\to (b\langle n\triangleleft x\rangle)[i]\le (b\langle n\triangleleft x\rangle)[i+1]

3.3 序列(sequencing)

依据霍尔规则:

Seq {P}c1{P}{P}c2{Q}{P}c1;c2{Q}Seq~\frac{\{P\}c_1\{P'\}\qquad\{P'\}c_2\{Q\}}{\{P\}c_1;c_2\{Q\}}

相应的谓词转换器即为:

wlp(c1;c2,Q)=wlp(c1,wlp(c2,Q))wlp(c_1;c_2,Q)=wlp(c_1,wlp(c_2,Q))

3.4 条件

依据霍尔规则:

相应的转换器即为:

3.5 while循环

依据等价关系:

相应的wlpwlp即为,此处略,最后转了个圈又回来了。

3.6 近似最弱前置条件

一般来说,我们无法总是算出循环的wlpwlp,比如上面的情况。但是,我们可以借助于循环不变式来近似它。

下面,我们使用这种方式表示循环:

while b do{I}cwhile~b~do\{I\}c

这里II是由程序员提供的循环不变量。

最为直观的想法是令:

wlp(while b do{I}c,Q)=Iwlp(while~b~do\{I\}c,Q)=I

但此时II可能不是最弱的前置条件。

如果我们草率地认为:

wlp(while b do{I}c,Q)=Iwlp(while~b~do\{I\}c,Q)=I

我们漏了两件事情:

  • 没有检查I¬bI\wedge\neg b得到QQ

  • 我们不知道II是否真的是一个循环不变式

所以我们需要构造一个额外的验证条件(verification condition)的集合:

为了在执行循环后确保QQ能够实现,需要满足两个条件:

  • 一是vc(while b doIc,Q)vc(while~b~do{I}c,Q)中的每一个公式都是永真的

  • 二是wlp(while b doIc,Q)=Iwlp(while~b~do{I}c,Q)=I一定是永真的

3.7 构造vc

while是唯一一个引入额外条件的命令,但是其他的声明可能也包含循环,所以:

vc(x:=a,Q)=vc(x:=a,Q)=\varnothing

vc(c1;c2,Q)=vc(c1,wlp(c2,Q))vc(c2,Q)vc(c_1;c_2,Q)=vc(c_1,wlp(c_2,Q))\cup vc(c_2,Q)

vc(if b then c1 else c2,Q)=vc(c1,Q)vc(c2,Q)vc(if~b~then~c_1~else~c_2,Q)=vc(c_1,Q)\cup vc(c_2,Q)

3.8 综合

综上,我们得到验证:

{P}c{Q}\{P\}c\{Q\}

的通用方法:

  1. 计算P=wlp(c,Q)P^{\prime}=wlp(c,Q)

  2. 计算vc(c,Q)vc(c,Q)

  3. 检查PPP\to P^{\prime} 的永真性

  4. 检查每个Fvc(c,Q)F\in vc(c,Q)的永真性

若3,4检验均通过,那么{P}c{Q}\lbrace P \rbrace c \lbrace Q \rbrace是永真的,但反之不一定成立,因为循环不变式可能不是最弱的前置条件。

上传的附件

发送私信

人生最好的三个词:久别重逢,失而复得,虚惊一场

48
文章数
33
评论数
最近文章
eject