程序验证（九）：程序正确性规范

本文主要是介绍程序验证（九）：程序正确性规范，希望对大家解决编程问题提供一定的参考价值，需要的开发者们随着小编来一起学习吧！

程序验证（九）：程序正确性规范

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

部分正确性(Partial Correctness)

部分正确性指的是一个程序的停止行为
我们将部分正确性用霍尔三元组(Hoare triples)表达：
{ P } c { Q } \{P\}c\{Q\} {P}c{Q}
这里：

• $c$是一个程序
• $P$和$Q$是一阶逻辑的断言(assertion)
• $P$, $Q$的自由变量可以在程序的变量中随意选择
• $P$是先验条件(precondition)，$Q$是后验条件(postcondition)
  { P } c { Q } \{P\}c\{Q\} {P}c{Q}的含义：
• 在一个满足$P$的环境中开始执行$c$
• 如果$c$终止
• 那么它的最终环境将满足$Q$
  注意，部分正确性没有排除以下两点：
• 程序执行不终止
• 程序没有从$P$开始执行

完全正确性(Total Correctness)

部分正确性没有要求终止
完全正确性是一个更强的声明，写作：
$$[P]c[Q]$$
$[P]c[Q]$的含义：

• 如果我们从一个满足$P$的环境开始执行$c$
• 那么$c$一定终止
• 而且它最终的环境满足$Q$

断言

给定三元组
{ P } c { Q } \{P\}c\{Q\} {P}c{Q}
公式$P$与$Q$是一阶断言
对于Imp，有用的理论是$T_Z\cup T_A$
$P$或$Q$中的变量包括程序变量、量词变量、其他逻辑变量，即
$$vars(Q)=pvars(Q)\cup qvars(Q)\cup lvars(Q)$$

断言的语义

由于$lvars(Q)$的存在，我们不能仅依据环境$\sigma$来判断$Q$的值
所以，令$\alpha$为$lvars(Q)$的变量的一个赋值，那么
$$(\alpha \cup \sigma )(x)\equiv \{\begin{array}{ll}\alpha (x)& ifx\in \alpha \\ \sigma (x)& ifx\in \sigma \end{array}$$
断言的可满足性与永真性：
$$\sigma {\models }_{\alpha }Q(\sigma \cup \alpha ){\models }_{T}Q\sigma satisfiesQunder\alpha$$
$$\sigma \models Q\forall \alpha .(\sigma \cup \alpha ){\models }_{T}QQisvalidin\sigma$$
如果对于所有$\sigma$，$\sigma \models Q$，那么我们写作$\models Q$

部分正确性的语义

我们说 { P } c { Q } \{P\}c\{Q\} {P}c{Q}在$\sigma$中在$\alpha$下永真，写作 σ ⊨ α { P } c { Q } \sigma\models_{\alpha} \{P\}c\{Q\} σ⊨α​{P}c{Q}，如果：
$$\forall {\sigma }^{\prime }.(\sigma {\models }_{\alpha }P\wedge ⟨c,\sigma ⟩\Downarrow {\sigma }^{\prime })\to {\sigma }^{\prime }{\models }_{\alpha }Q$$
也就是说：

1. 只要$\sigma$在$\alpha$下满足$P$
2. 而且$c$在$\sigma$中执行得到${\sigma }^{\prime }$
3. 那么${\sigma }^{\prime }$在$\alpha$下满足$Q$

我们说 { P } c { Q } \{P\}c\{Q\} {P}c{Q}是永真的，写作 ⊨ { P } c { Q } \models \{P\}c\{Q\} ⊨{P}c{Q}，如果：
∀ σ , α . σ ⊨ α { P } c { Q } \forall \sigma,\alpha.\sigma\models_{\alpha} \{P\}c\{Q\} ∀σ,α.σ⊨α​{P}c{Q}
也就是
$$\forall \sigma ,{\sigma }^{\prime },\alpha .(\sigma {\models }_{\alpha }P\wedge ⟨c,\sigma ⟩\Downarrow {\sigma }^{\prime })\to {\sigma }^{\prime }{\models }_{\alpha }Q$$

三元组的证明(verify)

我们将引入一种逻辑，该逻辑能从已知的三元组推出新的三元组，这种逻辑叫做霍尔逻辑(Hoare logic)
引入规则的形式为
⊢ { P } c { Q } \vdash \{P\}c\{Q\} ⊢{P}c{Q}

跳过与赋值(skip&assignment)

S k i p { P } s k i p { P } Skip~\frac{}{\{P\}\mathbf{skip}\{P\}} Skip {P}skip{P}​
A s g n { Q [ a / x ] } x : = a { Q } Asgn~ \frac{}{\{Q[a/x]\}x:=a\{Q\}} Asgn {Q[a/x]}x:=a{Q}​
$Q[a/x]$：在$Q$中把所有$x$换成$a$，举个例子：
$$(5+x)[(x+1)/x]=5+(x+1)$$

逻辑的加强与削弱

注意，我们不能证明一个很显而易见的东西：
⊢ { y = 0 } x : = 1 { x = 1 } \vdash\{y=0\}x:=1\{x=1\} ⊢{y=0}x:=1{x=1}
但我们可以证明：
⊢ { 1 = 1 } x : = 1 { x = 1 } \vdash\{1=1\}x:=1\{x=1\} ⊢{1=1}x:=1{x=1}
于是引入前提加强(precondition strengthening):
P r e ⊢ { P ′ } c { Q } P ⇒ P ′ { P } c { Q } Pre~\frac{\vdash\{P'\}c\{Q\}\qquad P\Rightarrow P'}{\{P\}c\{Q\}} Pre {P}c{Q}⊢{P′}c{Q}P⇒P′​
例如：
P r e A s g n ⊢ { 1 = 1 } x : = 1 { x = 1 } y = 0 ⇒ 1 = 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\}} Pre {y=0}x:=1{x=1}Asgn ⊢{1=1}x:=1{x=1}​y=0⇒1=1​
与之相似，引入一削弱后验条件的规则：
P o s t ⊢ { P } c { Q ′ } Q ′ ⇒ Q { P } c { Q } Post~\frac{\vdash\{P\}c\{Q'\}\qquad Q'\Rightarrow Q}{\{P\}c\{Q\}} Post {P}c{Q}⊢{P}c{Q′}Q′⇒Q​
在二者的基础上，引入序列规则(consequence rule):
C o n s e q P ⇒ P ′ ⊢ { P ′ } c { Q ′ } Q ′ ⇒ Q { P } c { Q } Conseq~\frac{P\Rightarrow P'\qquad\vdash \{P'\}c\{Q'\}\qquad Q'\Rightarrow Q}{\{P\}c\{Q\}} Conseq {P}c{Q}P⇒P′⊢{P′}c{Q′}Q′⇒Q​

组合(composition)

S e q { P } c 1 { P ′ } { P ′ } c 2 { Q } { P } c 1 ; c 2 { Q } Seq~\frac{\{P\}c_1\{P'\}\qquad \{P'\}c_2\{Q\}}{\{P\}c_1;c_2\{Q\}} Seq {P}c1​;c2​{Q}{P}c1​{P′}{P′}c2​{Q}​
举例：使用霍尔逻辑证明swap函数:
{ x = x ′ ∧ y = y ′ } t : = x ; x : = y ; y : = t { y = x ′ ∧ x = y ′ } \{x=x'\wedge y=y'\}t:=x;x:=y;y:=t\{y=x'\wedge x=y'\} {x=x′∧y=y′}t:=x;x:=y;y:=t{y=x′∧x=y′}

1. 由Asgn, { x = x ′ ∧ y = y ′ } t : = x { t = x ′ ∧ y = y ′ } \{x=x'\wedge y=y'\}t:=x\{t=x'\wedge y=y'\} {x=x′∧y=y′}t:=x{t=x′∧y=y′}
2. 由Asgn, { t = x ′ ∧ y = y ′ } x : = y { t = x ′ ∧ x = y ′ } \{t=x'\wedge y=y'\}x:=y\{t=x'\wedge x=y'\} {t=x′∧y=y′}x:=y{t=x′∧x=y′}
3. 由Asgn, { t = x ′ ∧ x = y ′ } y : = t { y = x ′ ∧ x = y ′ } \{t=x'\wedge x=y'\}y:=t\{y=x'\wedge x=y'\} {t=x′∧x=y′}y:=t{y=x′∧x=y′}
4. 由1，2，Seq, { x = x ′ ∧ y = y ′ } t : = x ; x : = y { t = x ′ ∧ x = y ′ } \{x=x'\wedge y=y'\}t:=x;x:=y\{t=x'\wedge x=y'\} {x=x′∧y=y′}t:=x;x:=y{t=x′∧x=y′}
5. 最后，由3，4，Seq,$$Q.E.D$$

条件(conditional)

I f { P ∧ b } c 1 { Q } { P ∧ ¬ b } c 2 { Q } { P } i f b t h e n c 1 e l s e c 2 { Q } If~\frac{\{P\wedge b\}c_1\{Q\}\qquad \{P\wedge \neg b\}c_2\{Q\}}{\{P\}\mathbf{if}~b~\mathbf{then}~c_1~\mathbf{else}~c_2\{Q\}} If {P}if b then c1​ else c2​{Q}{P∧b}c1​{Q}{P∧¬b}c2​{Q}​

• 在true分支：如果$b$成立，我们需要证明 { P ∧ b } c 1 { Q } \{P\wedge b\}c_1\{Q\} {P∧b}c1​{Q}
• 在false分支：如果$\neg b$成立，我们需要证明 { P ∧ ¬ b } c 2 { Q } \{P\wedge\neg b\}c_2\{Q\} {P∧¬b}c2​{Q}

while循环(loop)

W h i l e { P ∧ b } c { P } { P } w h i l e b d o c { P ∧ ¬ b } While~\frac{\{P\wedge b\}c\{P\}}{\{P\}\mathbf{while}~b~\mathbf{do}~c\{P\wedge\neg b\}} While {P}while b do c{P∧¬b}{P∧b}c{P}​

• $P$是循环不变量(loop invariant)
  • 在进入循环前成立，并且在每次迭代后保持不变
  • 这由前提 { P ∧ b } c { P } \{P\wedge b\}c\{P\} {P∧b}c{P}所确定
• 为了使用While，需要先证明$P$是不变量

可靠性与完备性

之前的规则对于部分正确性都是可靠的
对于Imp，是不完备的，因为可以归约为$T_{PA}$

这篇关于程序验证（九）：程序正确性规范的文章就介绍到这儿，希望我们推荐的文章对编程师们有所帮助！

---