程序验证(九):程序正确性规范

Tattoo

发布日期: 2020-07-02 09:43:51 浏览量: 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/106725080

什么是程序的正确性?应当在指定的前提下,进行预定的行为,达到指定的结果。

一、部分正确性(Partial Correctness)

部分正确性指的是一个程序的停止行为。

我们将部分正确性用霍尔三元组(Hoare triples)表达:

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

  • 其中cc是一个程序

  • 其中PPQQ是一阶逻辑的断言(assertion)

  • 其中P,QP, Q的自由变量可以在程序的变量中随意选择

  • 其中PP是先验条件(precondition),QQ是后验条件(postcondition)

上述{P}c{Q}\lbrace P \rbrace c \lbrace Q \rbrace的含义:

  • 在一个满足PP的环境中开始执行cc

  • 如果cc终止,那么它的最终环境将满足QQ

注意,部分正确性没有排除以下两点:

  • 程序执行不终止

  • 程序没有从PP开始执行

二、完全正确性(Total Correctness)

部分正确性没有要求终止,完全正确性是一个更强的声明,写作:

[P]c[Q][P]c[Q]

  • 如果我们从一个满足PP的环境开始执行cc

  • 那么cc一定终止,而且它最终的环境满足QQ

三、断言

给定三元组:

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

公式PPQQ是一阶断言。

对于Imp,有用的理论是TZTAT_Z\cup T_APPQQ中的变量包括程序变量、量词变量、其他逻辑变量,即

vars(Q)=pvars(Q)qvars(Q)lvars(Q)vars(Q)=pvars(Q)\cup qvars(Q)\cup lvars(Q)

3.1 断言的语义

由于lvars(Q)lvars(Q)的存在,我们不能仅依据环境σ\sigma来判断QQ的值,所以,令α\alphalvars(Q)lvars(Q)的变量的一个赋值,那么:

断言的可满足性与永真性:

如果对于所有σ\sigmaσQ\sigma\models Q,那么我们写作Q\models Q

3.2 部分正确性的语义

我们说{P}c{Q}\lbrace P \rbrace c \lbrace Q \rbraceσ\sigma中在α\alpha下永真,写作σα{P}c{Q}\sigma\models_{\alpha} \lbrace P \rbrace c \lbrace Q \rbrace,如果:

σ.(σαPc,σσ)σαQ\forall \sigma^{\prime}.(\sigma\models_{\alpha}P\wedge \langle c,\sigma\rangle\Downarrow\sigma^{\prime})\to\sigma^{\prime}\models_{\alpha}Q

也就是说:

  • 只要σ\sigmaα\alpha下满足PP

  • 而且ccσ\sigma中执行得到σ\sigma^{\prime}

  • 那么σ\sigma^{\prime}α\alpha下满足QQ

我们说{P}c{Q}\lbrace P \rbrace c \lbrace Q \rbrace是永真的,写作{P}c{Q}\models \lbrace P \rbrace c \lbrace Q \rbrace,如果:

σ,α.σα{P}c{Q}\forall \sigma,\alpha.\sigma\models_{\alpha} \{P\}c\{Q\}

也就是:

σ,σ,α.(σαPc,σσ)σαQ\forall \sigma,\sigma',\alpha. (\sigma\models_{\alpha}P\wedge\langle c,\sigma\rangle\Downarrow\sigma') \to \sigma'\models_{\alpha} Q

四、三元组的证明(verify)

我们将引入一种逻辑,该逻辑能从已知的三元组推出新的三元组,这种逻辑叫做霍尔逻辑(Hoare logic)。

引入规则的形式为:

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

4.1 跳过与赋值(skip&assignment)

Skip {P}skip{P}Skip~\frac{}{\{P\} skip \{P\}}

Asgn {Q[a/x]}x:=a{Q}Asgn~ \frac{}{\{Q[a/x]\}x:=a\{Q\}}

其中Q[a/x]Q[a/x]:在QQ中把所有xx换成aa,举个例子:

(5+x)[(x+1)/x]=5+(x+1)(5+x)[(x+1)/x]=5+(x+1)

4.2 逻辑的加强与削弱

注意,我们不能证明一个很显而易见的东西:

{y=0}x:=1{x=1}\vdash\{y=0\}x:=1\{x=1\}

但我们可以证明:

{1=1}x:=1{x=1}\vdash\{1=1\}x:=1\{x=1\}

于是引入前提加强(precondition strengthening):

Pre {P}c{Q}PP{P}c{Q}Pre~\frac{\vdash\{P'\}c\{Q\}\qquad P\Rightarrow P'}{\{P\}c\{Q\}}

例如:

Pre Asgn {1=1}x:=1{x=1}y=01=1{y=0}x:=1{x=1}Pre~\frac{Asgn~\frac{}{\vdash\{1=1\}x:=1\{x=1\}}\qquad y=0\Rightarrow 1=1}{\{y=0\}x:=1\{x=1\}}

与之相似,引入一削弱后验条件的规则:

Post {P}c{Q}QQ{P}c{Q}Post~\frac{\vdash\{P\}c\{Q'\}\qquad Q'\Rightarrow Q}{\{P\}c\{Q\}}

在二者的基础上,引入序列规则(consequence rule):

Conseq PP{P}c{Q}QQ{P}c{Q}Conseq~\frac{P\Rightarrow P'\qquad\vdash \{P'\}c\{Q'\}\qquad Q'\Rightarrow Q}{\{P\}c\{Q\}}

4.3 组合(composition)

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\}}

举例:使用霍尔逻辑证明swap函数

{x=xy=y}t:=x;x:=y;y:=t{y=xx=y}\{x=x'\wedge y=y'\}t:=x;x:=y;y:=t\{y=x'\wedge x=y'\}

1.由Asgn:

{x=xy=y}t:=x{t=xy=y}\{x=x'\wedge y=y'\}t:=x\{t=x'\wedge y=y'\}

2.由Asgn:

{t=xy=y}x:=y{t=xx=y}\{t=x'\wedge y=y'\}x:=y\{t=x'\wedge x=y'\}

3.由Asgn:

{t=xx=y}y:=t{y=xx=y}\{t=x'\wedge x=y'\}y:=t\{y=x'\wedge x=y'\}

4.由1,2,Seq:

{x=xy=y}t:=x;x:=y{t=xx=y}\{x=x'\wedge y=y'\}t:=x;x:=y\{t=x'\wedge x=y'\}

5.最后,由3,4,Seq:

Q.E.DQ.E.D

4.4 条件(conditional)

If {Pb}c1{Q}{P¬b}c2{Q}{P}if b then c1 else c2{Q}If~\frac{\{P\wedge b\}c_1\{Q\}\qquad \{P\wedge \neg b\}c_2\{Q\}}{\{P\} if~b~then~c_1~else~c_2\{Q\}}

  • 在true分支:如果bb成立,我们需要证明{Pb}c1Q\lbrace P\wedge b \rbrace c_1{Q}

  • 在false分支:如果¬b\neg b成立,我们需要证明{P¬b}c2{Q}\lbrace P\wedge\neg b \rbrace c_2 \lbrace Q \rbrace

4.5 while循环(loop)

While {Pb}c{P}{P}while b do c{P¬b}While~\frac{\{P\wedge b\}c\{P\}}{\{P\} while~b~do~c\{P\wedge\neg b\}}

其中,PP是循环不变量(loop invariant):

  • 在进入循环前成立,并且在每次迭代后保持不变

  • 这由前提{Pb}c{P}\lbrace P\wedge b \rbrace c \lbrace P \rbrace所确定

为了使用While,需要先证明PP是不变量。

五、可靠性与完备性

  • 之前的规则对于部分正确性都是可靠的

  • 对于Imp,是不完备的,因为可以归约为TPAT_{PA}

上传的附件

发送私信

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

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