程序验证（八）：形式语义

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

程序验证（八）：形式语义

语义描述方法

如下：

• 操作语义：用抽象机描述程序执行引起的状态改变，关心状态改变是怎样产生的，与语言的实现关系紧密。
• 指称语义：使程序执行的效果对应数学对象，只关心程序执行的效果，不关心其是怎样产生的。
• 公理语义：将程序的语义性质表示为命题，采用数理逻辑的方法研究。

引入玩具语言Imp

语法范畴

如下：

• 数字集$Num$，用$n$表示数字
• 变元集$Var$，用$x$表示变元
• 算术表达式集$Aexp$，用$a$表示算术表达式
• 布尔表达式集$Bexp$，用$b$表示布尔表达式
• 语句集$Com$，用$c$表示语句

语法

如下：
$$a\in AExp::=n\in \mathbb{Z}|x\in Var|a_1+a_2|a_1\ast a_2|a_1-a_2$$
$$b\in BExp::=\mathbf{t}\mathbf{r}\mathbf{u}\mathbf{e}|\mathbf{f}\mathbf{a}\mathbf{l}\mathbf{s}\mathbf{e}|a_1=a_2|a_1\le a_2|\neg b|b_1\wedge b_2$$
$$c\in Com::=\mathbf{s}\mathbf{k}\mathbf{i}\mathbf{p}|x:=a|c_1;c_2|\mathbf{i}\mathbf{f}b\mathbf{t}\mathbf{h}\mathbf{e}\mathbf{n}{c}_1\mathbf{e}\mathbf{l}\mathbf{s}\mathbf{e}{c}_2|\mathbf{w}\mathbf{h}\mathbf{i}\mathbf{l}\mathbf{e}b\mathbf{d}\mathbf{o}c$$

表达式语义

表达式的语义

采用二进制$$n::=0|1|n0|n1$$
语义函数$N:Num\to \mathbb{Z}$

• $N[0]=0$
• $N[1]=1$
• $N[n0]=2\ast N[0]$
• $N[n1]=2\ast N[n]+1$

状态

环境是从变元集到整数集的函数 $$Env=Var\to \mathbb{Z}$$

• 如$\sigma =[x\mapsto 5,y\mapsto 7,z\mapsto 0]$，即$\sigma x=5,\sigma y=7,\sigma z=0$
• 设${\sigma }^{\prime }=\sigma [x\mapsto 7]$，则${\sigma }^{\prime }x=7$，对于不同于$x$的变元$y$，${\sigma }^{\prime }y=\sigma y$
  状态是一个二元组$⟨c,\sigma ⟩$，其中$\sigma$是当前变量的赋值，$c$为下一条被执行的语句。

算术表达式的语义

语义函数$A:Aexp\to (Env\to \mathbb{Z})$:

• $A[n]\sigma =N[n]$
• $A[x]\sigma =\sigma x$
• $A[a_1+a_2]\sigma =A[a_1]\sigma +A[a_2]\sigma$
• $A[a_1\ast a_2]\sigma =A[a_1]\sigma \ast A[a_2]\sigma$
• $A[a_1-a_2]\sigma =A[a_1]\sigma -A[a_2]\sigma$

布尔表达式的语义

语义函数$B:Bexp\to (Env\to T)$：

• $B[true]\sigma =\mathbf{t}\mathbf{r}\mathbf{u}\mathbf{e}$
• $B[false]\sigma =\mathbf{f}\mathbf{a}\mathbf{l}\mathbf{s}\mathbf{e}$
• $B[a_1=a_2]\sigma =A[a_1]\sigma =A[a_2]\sigma$
• $B[a_1\le a_2]\sigma =A[a_1]\sigma \le A[a_2]\sigma$
• $B[\neg b]\sigma =\neg B[b]\sigma$
• $B[b_1\wedge b_2]\sigma =B[b_1]\sigma \wedge B[b_2]\sigma$

举例

在环境$\sigma =[x\mapsto 1,y\mapsto 3]$下计算表达式$(x+2)\ast y$的值
$$A[(x+2)\ast y]\sigma =A[(x+2)]\sigma \ast A[y]\sigma =(A[x]\sigma +A[2]\sigma )\ast A[y]\sigma =(1+2)\ast 3=9$$

代入

用算术表达式$a_0$替换算术表达式$a$中变元$y$的所有出现得到的算术表达式记为$a[y\mapsto a_0]$
$$A[a[y\mapsto a_0]]\sigma =A[a](\sigma [y\mapsto A[a_0]\sigma ])$$
用算术表达式$a_0$替换布尔表达式$b$中变元$y$的所有出现得到的布尔表达式记为$b[y\mapsto a_0]$
$$B[b[y\mapsto a_0]]\sigma =B[b](\sigma [y\mapsto A[a_0]\sigma ])$$

操作语义

概念

包括以下两种：

• 结构操作语义（小步操作语义）：描述执行语句的各步计算如何发生
• 自然语义（大步操作语义）：描述如何得到语句执行终止的最终状态

结构操作语义

结构操作语义强调计算的具体步骤，基于状态之间的迁移关系$\to$来定义，即
$$⟨c,\sigma ⟩\to ⟨c^{\prime },{\sigma }^{\prime }⟩$$
意义：语句$c$从环境$\sigma$执行到中途，这时环境为${\sigma }^{\prime }$，待执行的语句为$c^{\prime }$
反复应用上面的迁移关系，直至程序终止状态$⟨\mathbf{s}\mathbf{k}\mathbf{i}\mathbf{p},\sigma ⟩$
若无状态$⟨c^{\prime },{\sigma }^{\prime }⟩$使得$⟨c,\sigma ⟩\to ⟨c^{\prime },{\sigma }^{\prime }⟩$，则称$⟨c,\sigma ⟩$是呆滞的(stuck)

Imp的结构操作语义

$$Asgn:\frac{}{⟨x:=a,\sigma ⟩\to ⟨\mathbf{s}\mathbf{k}\mathbf{i}\mathbf{p},\sigma [x\mapsto A[a]\sigma ]⟩}$$
$$Skip:norule$$
$$Seq1:\frac{⟨c_1,\sigma ⟩\to ⟨c_1^{\prime },{\sigma }_1^{\prime }⟩}{⟨c_1;c_2,\sigma ⟩\to ⟨c_1^{\prime };c_2,{\sigma }^{\prime }⟩}$$
$$Seq2:\frac{}{⟨\mathbf{s}\mathbf{k}\mathbf{i}\mathbf{p};c,\sigma ⟩\to ⟨c,\sigma ⟩}$$
$$IfTrue:\frac{}{⟨\mathbf{i}\mathbf{f}b\mathbf{t}\mathbf{h}\mathbf{e}\mathbf{n}{c}_1\mathbf{e}\mathbf{l}\mathbf{s}\mathbf{e}{c}_2,\sigma ⟩\to ⟨c_1,\sigma ⟩}$$
$$IfFalse:\frac{}{⟨\mathbf{i}\mathbf{f}b\mathbf{t}\mathbf{h}\mathbf{e}\mathbf{n}{c}_1\mathbf{e}\mathbf{l}\mathbf{s}\mathbf{e}{c}_2,\sigma ⟩\to ⟨c_2,\sigma ⟩}$$
$$While:\frac{}{⟨\mathbf{w}\mathbf{h}\mathbf{i}\mathbf{l}\mathbf{e}b\mathbf{d}\mathbf{o}c,\sigma ⟩\to ⟨\mathbf{i}\mathbf{f}b\mathbf{t}\mathbf{h}\mathbf{e}\mathbf{n}(c;\mathbf{w}\mathbf{h}\mathbf{i}\mathbf{l}\mathbf{e}b\mathbf{d}\mathbf{o}c)\mathbf{e}\mathbf{l}\mathbf{s}\mathbf{e}\mathbf{s}\mathbf{k}\mathbf{i}\mathbf{p},\sigma }$$

推导序列

语句$c$从环境$\sigma$开始的推导序列有以下两种形式（记${\gamma }_0=⟨c,\sigma ⟩$）：

• 有限状态序列${\gamma }_0,{\gamma }_1,\dots ,{\gamma }_k$，其中${\gamma }_0\to {\gamma }_1,\dots ,{\gamma }_{k-1}\to {\gamma }_k$可以推导得出。${\gamma }_k$的形式为$⟨\mathbf{s}\mathbf{k}\mathbf{i}\mathbf{p},{\sigma }^{\prime }⟩$或者${\gamma }_k$是呆滞的。
• 无限状态序列${\gamma }_0,{\gamma }_1,\dots$，其中${\gamma }_0\to {\gamma }_1$, ${\gamma }_1\to {\gamma }_2$等可以推导得到。
• 将${\gamma }_0\to {\gamma }_1\to \cdots \to {\gamma }_k$简记为${\gamma }_0{\to }^{\ast }{\gamma }_k$

确定性

结构操作语义具有确定性：对于任意语句$c$，从任意环境$\sigma$出发，只要$⟨c,\sigma ⟩\to ⟨c^{\prime },{\sigma }^{\prime }⟩$且$⟨c,\sigma ⟩\to ⟨c^{\prime \prime },{\sigma }^{\prime \prime }⟩$，就有$c^{\prime }=c^{\prime \prime },{\sigma }^{\prime }={\sigma }^{\prime \prime }$

终止和循环

若存在从状态$⟨c,\sigma ⟩$开始的有限推导序列，则称语句$c$从环境$\sigma$执行是终止的。
若存在从状态$⟨c,\sigma ⟩$开始的无限推导序列，则称语句$c$从环境$\sigma$执行是循环的。
若语句$c$从每个环境执行都是终止的，则称语句$c$总是终止的。
若语句$c$从每个环境执行都是循环的，则称语句$c$总是循环的。

语义等价

如果对于任意状态$\sigma$，满足下列条件：

• 对于任意终止或呆滞格局$⟨c^{\prime },{\sigma }^{\prime }⟩$，$⟨c_1,\sigma ⟩{\to }^{\ast }⟨c^{\prime },{\sigma }^{\prime }⟩$，当且仅当$⟨c_2,\sigma ⟩{\to }^{\ast }⟨c^{\prime },{\sigma }^{\prime }⟩$
• 存在从$⟨c_1,\sigma ⟩$开始的无限推导序列当且仅当存在从$⟨c_2,\sigma ⟩$开始的无限推导序列
  则称语句$c_1$和$c_2$是语义等价的，如语句$c_1;(c_2;c_3)$和语句$(c_1;c_2);c_3$是语义等价的。

语义函数

可将语句$c$的意义概括为从$Env$到$Env$的部分函数：
$$S_{SOS}:Cmd\to (Env\hookrightarrow Env)$$
定义$$S_{SOS}[c]\sigma =\{\begin{array}{ll}{\sigma }^{\prime }& if⟨c,\sigma ⟩{\to }^{\ast }⟨\mathbf{s}\mathbf{k}\mathbf{i}\mathbf{p},{\sigma }^{\prime }⟩\\ undef& otherwise\end{array}$$
例如，$S_{SOS}[\mathbf{w}\mathbf{h}\mathbf{i}\mathbf{l}\mathbf{e}\mathbf{t}\mathbf{r}\mathbf{u}\mathbf{e}\mathbf{d}\mathbf{o}\mathbf{s}\mathbf{k}\mathbf{i}\mathbf{p}]\sigma =undef$

自然语义

自然语义关心语句执行对环境的改变。
从环境$\sigma$执行语句$c$将终止于环境${\sigma }^{\prime }$:
$$⟨c,\sigma ⟩\Downarrow {\sigma }^{\prime }$$
规则的一般形式：
$$\frac{⟨c_1,{\sigma }_1⟩\Downarrow {\sigma }^{\prime },\dots ,⟨c_n,{\sigma }_n⟩\Downarrow {\sigma }_n^{\prime }}{⟨c,\sigma ⟩\Downarrow {\sigma }^{\prime }}if\dots$$

Imp的自然语义

$$BigAsgn:\frac{}{⟨x:=a,\sigma ⟩\Downarrow \sigma [x\to A[a]\sigma ]}$$
$$BigSkip:\frac{}{⟨\mathbf{s}\mathbf{k}\mathbf{i}\mathbf{p},\sigma ⟩\Downarrow \sigma }$$
$$BigSeq:\frac{⟨c_1,{\sigma }_1⟩\Downarrow {\sigma }_1^{\prime }⟨c_2,{\sigma }_1^{\prime }⟩\Downarrow {\sigma }_2}{⟨c_1;c_2,{\sigma }_1⟩\Downarrow {\sigma }_2}$$
$$BigIfT:\frac{⟨c_1,\sigma ⟩\Downarrow {\sigma }^{\prime }}{⟨\mathbf{i}\mathbf{f}b\mathbf{t}\mathbf{h}\mathbf{e}\mathbf{n}{c}_1\mathbf{e}\mathbf{l}\mathbf{s}\mathbf{e}{c}_2,\sigma ⟩\Downarrow {\sigma }^{\prime }}ifB[b]\sigma =\mathbf{t}\mathbf{r}\mathbf{u}\mathbf{e}$$
$$BigIfF:\frac{⟨c_2,\sigma ⟩\Downarrow {\sigma }^{\prime }}{⟨\mathbf{i}\mathbf{f}b\mathbf{t}\mathbf{h}\mathbf{e}\mathbf{n}{c}_1\mathbf{e}\mathbf{l}\mathbf{s}\mathbf{e}{c}_2,\sigma ⟩\Downarrow {\sigma }^{\prime }}ifB[b]\sigma =\mathbf{f}\mathbf{a}\mathbf{l}\mathbf{s}\mathbf{e}$$
$$BigWhileFalse:\frac{}{⟨\mathbf{w}\mathbf{h}\mathbf{i}\mathbf{l}\mathbf{e}b\mathbf{d}\mathbf{o}c,\sigma ⟩\Downarrow \sigma }ifB[b]\sigma =\mathbf{f}\mathbf{a}\mathbf{l}\mathbf{s}\mathbf{e}$$
$$BigWhileTrue\frac{⟨c,\sigma ⟩\Downarrow {\sigma }^{\prime }⟨\mathbf{w}\mathbf{h}\mathbf{i}\mathbf{l}\mathbf{e}b\mathbf{d}\mathbf{o}c,{\sigma }^{\prime }⟩\Downarrow {\sigma }^{\prime \prime }}{⟨\mathbf{w}\mathbf{h}\mathbf{i}\mathbf{l}\mathbf{e}b\mathbf{d}\mathbf{o}c,\sigma ⟩\Downarrow {\sigma }^{\prime \prime }}ifB[b]\sigma =\mathbf{t}\mathbf{r}\mathbf{u}\mathbf{e}$$
每个规则有若干前提和一个结论。称有0个前提的规则为公理，如BigAsgn, BigSkip, BigWhileFalse是公理。
当使用公理和规则得出$⟨c,\sigma ⟩\Downarrow {\sigma }^{\prime }$时，就得到一推导树，树根是$⟨c,\sigma ⟩\Downarrow {\sigma }^{\prime }$，树叶是公理，每个分支点是某规则的结论，而它的儿子是该规则的前提。

终止和循环

若存在环境${\sigma }^{\prime }$使得$⟨c,\sigma ⟩\Downarrow {\sigma }^{\prime }$，则称语句$c$从环境$\sigma$执行是终止的。
若不存在环境${\sigma }^{\prime }$使得$⟨c,\sigma ⟩\Downarrow {\sigma }^{\prime }$，则称语句$c$从环境$\sigma$执行是循环的。
若语句$c$从每个环境执行都是终止的，则称语句$c$总是终止的。
若语句$c$从每个环境执行都是循环的，则称语句$c$总是循环的。

语义等价

如果对于任意环境$\sigma$和${\sigma }^{\prime }$:
$$⟨c_0,\sigma ⟩\Downarrow {\sigma }^{\prime }\iff ⟨c_1,\sigma ⟩\Downarrow {\sigma }^{\prime }$$
则称语句$c_0$和$c_1$是语义等价的。

确定性

自然语义具有确定性：对于任意语句$c$，和任意环境${\sigma }_1,{\sigma }_2,\sigma$，只要$⟨c,\sigma ⟩\Downarrow {\sigma }_1$且$⟨c,\sigma ⟩\Downarrow {\sigma }_2$，就有${\sigma }_1={\sigma }_2$，即
$$\forall \sigma ,{\sigma }_1,{\sigma }_2,c.(⟨c,\sigma ⟩\Downarrow {\sigma }_1\wedge ⟨c,\sigma ⟩\Downarrow {\sigma }_2)\to ({\sigma }_1={\sigma }_2)$$

语义函数

可将语句$c$的意义概括为从$Fnv$到$Env$的部分函数：
$$S_{ns}:Cmd\to (Env\hookrightarrow Env)$$
定义$$S_{ns}[c]\sigma =\{\begin{array}{ll}{\sigma }^{\prime }& if⟨c,\sigma ⟩\Downarrow {\sigma }^{\prime }\\ undef& otherwise\end{array}$$

两种语义的对比

等价性
对于语言Imp的每个语句$c$，任意环境$\sigma$和${\sigma }^{\prime }$，若$⟨c,\sigma ⟩\Downarrow {\sigma }^{\prime }$，则$⟨c,\sigma ⟩{\to }^{\ast }⟨\mathbf{s}\mathbf{k}\mathbf{i}\mathbf{p},{\sigma }^{\prime }⟩$
对于语言Imp的每个语句$c$，任意环境$\sigma$和${\sigma }^{\prime }$，若$⟨c,\sigma ⟩{\to }^k⟨\mathbf{s}\mathbf{k}\mathbf{i}\mathbf{p},{\sigma }^{\prime }⟩$，则$⟨c,\sigma ⟩\Downarrow {\sigma }^{\prime }$
对于语言Imp的每个语句$c$，
$$S_{ns}[c]=S_{SOS}[c]$$

这篇关于程序验证（八）：形式语义的文章就介绍到这儿，希望我们推荐的文章对编程师们有所帮助！

---