形式语义学学习笔记

发表于 | 分类于

这学期上whp老师的形式语义学课程，做一些简单的记录.

教材：The Formal Semantics of Programming Languages_ An Introduction. Gylnn Winskel.

  • IMP: Simple Imperative Language
  • 操作语义：MOS & SOS
  • 指称语义：Denotational Semantics
  • 公理语义：Hoare Logic

IMP: a Simple Imperative Language

IMP的指令分为 \(\mathbf{Aexp}\)（算术表达式）, \(\mathbf{Bexp}\)（布尔表达式）, 以及 \(\mathbf{Com}\)（命令）三部分. 其抽象语法如下所示：

其中 \(n\) 为整数，\(X\) 为地址.

  • \(\mathbf{Aexp}\) \(a::=n ~|~ X ~|~ a_1+a_2 ~|~ a_1-a_2 ~|~ a_1\times a_2\);
  • \(\mathbf{Bexp}\) \(b::=\mathbf{true} ~|~ \mathbf{false} ~|~ a_{0}=a_{1} ~|~ a_{0} \leq a_{1} ~|~ \neg b ~|~ b_{0} \wedge b_{1} ~|~ b_{0} \vee b_{1}\);
  • \(\mathbf{Com}\) \(c::=\mathbf{skip} ~|~ X:=a ~|~ \mathbf{if}~b~\mathbf{then}~c_{0}~\mathbf{else}~c_{1}~|~\mathbf{while}~b~\mathbf{do}~c ~|~ c_{0};~c_{1}\);

举一个 IMP 的例子吧…计算阶乘：

\[ \begin{align*} fu&nc~\mathbf{Factorial}~X~:\\ &Y := 1;\\ &\mathbf{while}~\neg(X=0)~\mathbf{do}\\ &\quad Y:=Y\times X;\\ &\quad X:=X-1\\ &\mathbf{end} \end{align*} \]

形式语义学可以对 IMP 的语义做一些解释，进而完成程序的形式化验证等工作.

操作语义

操作语义首先规定了系统的状态，然后把指令视作系统状态间的转移（操作）.

SDEC Machine: Stack-Environment-Device-Control 四元组：

  • Stack：堆栈，记为 \(s\);
  • Environment：记录系统外的环境，记为 \(e\);
  • Device：记录存储的东西，记为 \(d\);
  • Control：存储命令，记为 \(c\).

事实上，描述 IMP 的语义只需要 \((s,d,c)\) 机器就够了：

  • \(s \in(\mathbb{N} \cup\{\mathbf{T}, \mathbf{F}\} \cup \mathbf{Loc} \cup \mathbf{Com})^{*}\);
  • \(d \in \mathbf{Loc} \longrightarrow \mathbb{N}\); 地址 -> 地址存储的值.
  • \(c \in(\mathbf { Aexp } \cup \mathbf { Bexp } \cup \mathbf { Com } \cup \mathbf { Cs })^{*}\)，其中 \(\mathbf{Cs}=\{\mathbf { if, while }, \rightarrow, ;,+,-, x,=, \leq, \neg, \vee, \wedge\}\).

操作语义分为 SOS 和 MOS 两个路数

SOS: Structural Operational Semantics

\(\mathbf{Aexp}\) 的求值

  • 数字/地址：\[\langle n,\sigma\rangle\longrightarrow n\qquad \langle X,\sigma\rangle\longrightarrow \sigma(X)\]
  • 求和：（其中 \(n\) 是 \(n_1\) 与 \(n_2\) 的和，减法乘法同理）\[\frac{\left\langle a_{0}, \sigma\right\rangle \longrightarrow n_{0} \quad\left\langle a_{1}, \sigma\right\rangle \longrightarrow n_{1} }{\left\langle a_{0}+a_{1}, \sigma\right\rangle \longrightarrow n}\]

\(\mathbf{Bexp}\) 的求值

  • 真值：（注意，\(\mathbf{true}\) 是一个语法对象，但 \(\mathrm{T}\) 是一个语义中的真值）\[\langle\mathbf { true }, \sigma\rangle \longrightarrow \mathrm{T}, \quad\langle\mathbf { false }, \sigma\rangle \longrightarrow \mathrm{F}\]
  • 判断：（以 \(=\) 为例，\(\leqslant\) 同理）\[\begin{align} \frac{\langle a_0,\sigma\rangle\longrightarrow n_0\quad\langle a_1,\sigma\rangle\longrightarrow n_1}{\langle a_0=a_1,\sigma\rangle\longrightarrow \mathrm{T} }, &\quad 若~n_0~与~n_1~\text{相等}\\ \frac{\langle a_0,\sigma\rangle\longrightarrow n_0\quad\langle a_1,\sigma\rangle\longrightarrow n_1}{\langle a_0=a_1,\sigma\rangle\longrightarrow \mathrm{F} }, &\quad 若~n_0~与~n_1~\text{不等} \end{align}\]
  • 取反：\[\frac{\langle b,\sigma\rangle\longrightarrow\mathrm{T} }{\langle \neg b,\sigma\rangle\longrightarrow\mathrm{F} }\qquad\frac{\langle b,\sigma\rangle\longrightarrow\mathrm{F} }{\langle \neg b,\sigma\rangle\longrightarrow\mathrm{T} }\]
  • 二元逻辑运算：（以 \(\wedge\) 为例，其中 \(t=\begin{cases}\mathrm{T}\quad \text{if}~t_1\equiv t_2\equiv \mathrm{T} \\ \mathrm{F}\quad\text{otherwise} \end{cases}\)，\(\vee\) 同理. 其实和 \(\mathbf{Aexp}\) 中的加法也是同理）\[\begin{align*}\frac{\left\langle b_{0}, \sigma\right\rangle \longrightarrow t_{0} \quad\left\langle b_{1}, \sigma\right\rangle \longrightarrow t_{1} }{\langle b_0\wedge b_1,\sigma \rangle\longrightarrow t}\end{align*}\]

\(\mathbf{Com}\) 的执行

\[ \begin{align*} \mathrm{Skip}~\frac{}{\langle \mathbf{skip},\sigma\rangle\longrightarrow\sigma} \qquad&\qquad\qquad\qquad\mathrm{Assign}~\frac{\langle a,\sigma\rangle\longrightarrow n}{\langle X:=a,\sigma\rangle\longrightarrow\sigma[n/X]} \\ \mathrm{If}~\frac{\langle b,\sigma\rangle\longrightarrow \mathrm{T}\quad \langle c_0,\sigma\rangle\longrightarrow\sigma'}{\langle \mathbf{if}~b~\mathbf{then}~c_0~\mathbf{else}~c_1,\sigma \rangle\longrightarrow\sigma'} &\qquad\qquad\qquad \mathrm{If}~\frac{\langle b,\sigma\rangle\longrightarrow \mathrm{F}\quad \langle c_1,\sigma\rangle\longrightarrow\sigma'}{\langle \mathbf{if}~b~\mathbf{then}~c_0~\mathbf{else}~c_1,\sigma \rangle\longrightarrow\sigma'} \\ \mathrm{While}~\frac{\langle b,\sigma\rangle\longrightarrow\mathrm{F} }{\langle \mathbf{while}~b~\mathbf{do}~c,\sigma \rangle\longrightarrow\sigma} &\qquad \mathrm{While}~\frac{\langle b,\sigma\rangle\longrightarrow\mathrm{T} \quad \langle c,\sigma\rangle\longrightarrow\sigma' \quad \langle \mathbf{while}~b~\mathbf{do}~c,\sigma' \rangle\longrightarrow\sigma''}{\langle \mathbf{while}~b~\mathbf{do}~c,\sigma \rangle\longrightarrow\sigma''} \end{align*} \]

SOS 的性质

  1. 确定性：SOS 具有确定性. 其中 \(\mathbf{Com}\) 的确定性证明用到了良基归纳（Well-founded induction）.
    • 关于 well-founded induction 不多赘述.
  2. 终止性：\(\mathbf{Aexp}\) 和 \(\mathbf{Bexp}\) 是终止的，但 \(\mathbf{Com}\) 是不终止的.

MOS: Mechanical Operational Semantics

\(\mathbf{Aexp}\) 的语义

  • 数字/地址：\[(s,d,nc') \longrightarrow (ns, d, c')\qquad (s,d, Xc') \longrightarrow (d(X)s,d,c')\]

  • 运算：（其中 \(n\) 是 \(n_1\) 与 \(n_2\) 的和，减法乘法同理）\[\begin{align*}(s,d,(a_1+a_2)c') &\longrightarrow (s,d,a_1a_2+c')\\ (n_2n_1s,d,+c')&\longrightarrow (ns, d, c')\end{align*}\]

  • 真值：\[\begin{align*} (s,d,\mathbf{true}c') &\longrightarrow (\mathrm{T}s, d, c') \\ (s,d,\mathbf{false}c') &\longrightarrow (\mathrm{F}s, d, c') \end{align*}\]
  • 比较：（以 \(=\) 为例，\(\leqslant\) 同理）\[\begin{align*} (s,d,(a_1=a_2)c')&\longrightarrow(s,d,a_1a_2=c') \\ (n_2n_1s,d,=c')&\longrightarrow (\mathrm{T}s,d,c')\quad \text{if}~n_1=n_2 \\ (n_2n_1s,d,=c')&\longrightarrow (\mathrm{F}s,d,c')\quad \text{if}~n_1\neq n_2 \\ \end{align*}\]
  • 取反：\[\begin{align*} (s,d,(\neg b)c') &\longrightarrow (s,d,b\neg c') \\ (\mathrm{T}s, d, \neg c') &\longrightarrow (\mathrm{F}s, d, c') \\ (\mathrm{F}s, d, \neg c') &\longrightarrow (\mathrm{T}s, d, c') \end{align*}\]

  • 二元逻辑运算：（以 \(\wedge\) 为例，其中 \(t=\begin{cases}\mathrm{T}\quad \text{if}~t_1=t_2=\mathrm{T} \\ \mathrm{F}\quad\text{otherwise} \end{cases}\)，\(\vee\) 同理. 其实和 \(\mathbf{Aexp}\) 中的加法也是同理）\[\begin{align*} \left(s, d,\left(b_{1} \wedge b_{2}\right) c^{\prime}\right) &\longrightarrow\left(s, d, b_{1} b_{2} \wedge c^{\prime}\right)\\ (t_2t_1s, d, \wedge c') &\longrightarrow (ts, d, c') \\ \end{align*}\]

\(\mathbf{Com}\) 的语义

  • 空语句：\[(s,d,\mathbf{skip}~c')\longrightarrow(s,d,c')\]
  • 赋值：\[\begin{align*} (s,d,X:=a~c') &\longrightarrow (Xs, d, a\rightarrow c') \\ (nXs, d, \rightarrow c') &\longrightarrow (s, d[n/X], c') \end{align*}\]
  • 顺序：\[\begin{align*} (s, d, (c_0;~c_1)c') &\longrightarrow (s,d,c_0;~(c_1c')) \\ (s', d', ;~c'') &\longrightarrow (s', d', c'') \end{align*}\]
  • 条件：\[\begin{align*} (s, d, (\mathbf{if}~b~\mathbf{then}~c_0~\mathbf{else}~c_1) c') &\longrightarrow (c_0c_1s, d, b~\mathbf{if}~c')\\ (\mathrm{T}c_0c_1s, d, \mathbf{if}~c') &\longrightarrow (s,d,c_0c') \\ (\mathrm{F}c_0c_1s, d, \mathbf{if}~c') &\longrightarrow (s,d,c_1c') \end{align*}\]
  • 循环：\[\begin{align*} (s, d, (\mathbf{while}~b~\mathbf{do}~c)c') &\longrightarrow ((c;~\mathbf{while}~b~\mathbf{do}~c)s, d, b~\mathbf{while}~c')\\ (\mathrm{T}(c;~\mathbf{while}~b~\mathbf{do}~c)s, d, \mathbf{while}~c') &\longrightarrow (s,d,(c;~\mathbf{while}~b~\mathbf{do}~c)c') \\ (\mathrm{F}(c;~\mathbf{while}~b~\mathbf{do}~c)s, d, \mathbf{while}~c') &\longrightarrow (s,d,c') \end{align*}\]

MOS 的性质

  1. 确定性：上述 MOS 所规定的的转移 \(\rightarrow\) 是确定的，i.e. 若 \((s_0,d_0,c_0)\to(s_1,d_1,c_1)\) 且 \((s_0,d_0,c_0)\to(s_2,d_2,c_2)\)，则有 \((s_1,d_1,c_1)=(s_2,d_2,c_2)\)
    • 证明挺容易的（
  2. 终止性：\(\mathbf{Aexp}\) 和 \(\mathbf{Bexp}\) 都是终止的，但 \(\mathbf{Com}\) 不是（例如 \(\mathbf{while~true~do~skip}\)）.

这两条应该都和 SOS 一样.

现定义二元关系 \((s,d,c)\rightarrow^* (s',d',c')\)，表示存在一个序列 \(\left\{\left(s_{i}, d_{i}, c_{i}\right)\right\}_{i=1}^{n}\)，s.t. \[(s, d, c)=\left(s_{1}, d_{1}, c_{1}\right) \rightarrow \cdots \rightarrow\left(s_{n}, d_{n}, c_{n}\right)=\left(s^{\prime}, d^{\prime}, c^{\prime}\right)\] 则易得：

  • \(\rightarrow^*\) 是自反的；
  • \(\rightarrow^*\) 是传递的；
  • 但 \(\rightarrow^*\) 不是确定的.

事实上，\(\rightarrow^*\) 具有另一种意义下的确定性，称为 Church-Rosser Property：

若 \((s,d,c)\rightarrow^* (s',d',c')\) 且 \((s,d,c)\rightarrow^* (s'',d'',c'')\)，则存在 \((\bar{s},\bar{d},\bar{c})\)，s.t. \((s',d',c') \rightarrow^* (\bar{s},\bar{d},\bar{c})\) 且 \((s'',d'',c'') \rightarrow^* (\bar{s},\bar{d},\bar{c})\).

还可以定义第三种关系 \(\rightarrow'\)，表示 \(\rightarrow^*\) 的中间序列不为空，即“至少经过一步转移”. 不过我感觉好像没什么意义…这东西破坏了自反性和 Church-Rosser 性质…

指称语义

新的记号

  • 状态集：\(\Sigma\)；一个指称就是从状态集到“意思”集合的映射.
  • 全函数 \(A\to B\)：每个 \(a\in A\) 都有像；
  • 部分函数 \(A\rightharpoonup B\)：不是每个 \(a\in A\) 都有像.

\(\mathbf{Aexp}\) 的语义

实际上是定义了一个 \(\mathbf{Aexp}\) 到其指称的映射 \(\mathcal{A}: \mathbf{Aexp}\to (\Sigma\to\mathbb{N})\). （\(\mathbf{Bexp}\) 同理）

  • 数字/地址：\[\mathcal{A}[ [n] ](\sigma)=n\qquad \mathcal{A}[ [X] ](\sigma)=\sigma(X)\]
  • 加法：（减法和乘法同理）\[\mathcal{A}[ [a_1+a_2] ]=\mathcal{A}[ [a_1] ]+\mathcal{A}[ [a_2 ]]\]

\(\mathbf{Bexp}\) 的语义

  • 真值/地址：\[\mathcal{B}[ [\mathbf{true}] ](\sigma)=\mathrm{T}\qquad \mathcal{B}[ [\mathbf{false}] ](\sigma)=\mathrm{F}\qquad \mathcal{B}[ [X] ](\sigma)=\sigma(X)\]
  • 判断：（以 \(=\) 为例，\(\leqslant\) 同理）\[\mathcal{B}[ [a_1=a_2] ]=\begin{cases} \mathrm{T}\quad 若~\mathcal{A}[ [a_1] ](\sigma)=\mathcal{A}[ [a_2] ](\sigma)\\ \mathrm{F}\quad 若~\mathcal{A}[ [a_1] ](\sigma)\neq\mathcal{A}[ [a_2] ](\sigma) \end{cases}\]
  • 逻辑运算：（\(\vee\) 同理）\[\mathcal{B}[ [\neg b] ](\sigma)=\neg\mathcal{B}[ [b] ](\sigma)\qquad \mathcal{B}[ [b_1\wedge b_2] ](\sigma)=\mathcal{B}[ [b_1] ](\sigma)\wedge \mathcal{B} [[b_2] ](\sigma)\]

\(\mathbf{Com}\) 的语义

命令的指称是部分函数 \(\Sigma\rightharpoonup\Sigma\)（因为有一些命令并不终止），因此其指称语义是 \(\mathcal{C}:\mathbf{Com}\to(\Sigma\rightharpoonup\Sigma)\).

  • 空语句/赋值：\[\mathcal{C}[ [\mathbf{skip}] ](\sigma)=\sigma \qquad \mathcal{C}[ [X:=a ]](\sigma)=\sigma(n/X)\]
  • 顺序：\[\mathcal{C}[ [c_1;~c_2] ](\sigma)=\mathcal{C}[ [c_2] ](\mathcal{C}[ [c_1 ]](\sigma))=(\mathcal{C}[ [c_2] ]\circ\mathcal{C}[ [c_1] ])(\sigma)\]
  • 条件：\[\mathcal{C}[ [\mathbf{if}~b~\mathbf{then}~c_0~\mathbf{else}~c_1] ](\sigma)=\begin{cases} \mathcal{C}[ [c_0] ](\sigma)\quad 若~\mathcal{B}[ [b] ](\sigma)=\mathrm{T} \\ \mathcal{C}[ [c_1] ](\sigma)\quad 若~\mathcal{B}[ [b] ](\sigma)=\mathrm{F} \end{cases}\]
  • 循环：\[\begin{align*} \mathcal{C}[ [\mathbf{while}~b~\mathbf{do}~c] ](\sigma)&= \begin{cases} \sigma & 若~\mathcal{B}[ [b] ](\sigma)=\mathrm{F}\\ \mathcal{C}[ [\mathbf{while}~b~\mathbf{do}~c] ](\mathcal{C}[ [c] ](\sigma)) & 若~\mathcal{B}[ [b] ](\sigma)=\mathrm{T} \end{cases} \\ &=\begin{cases} \sigma & 若~\mathcal{B}[ [b] ](\sigma)=\mathrm{F}\\ (\mathcal{C}[ [\mathbf{while}~b~\mathbf{do}~c] ]\circ\mathcal{C}[ [c] ])((\sigma)) & 若~\mathcal{B}[ [b] ](\sigma)=\mathrm{T} \end{cases} \end{align*}\]

\(\mathcal{C}[ [\mathbf{while}~b~\mathbf{do}~c] ]\) 的存在性与唯一性

定义函数： \[F:(\Sigma\rightharpoonup\Sigma)\to(\Sigma\rightharpoonup\Sigma),\quad F(\varphi)(\sigma)=\begin{cases} \sigma & 若~\mathcal{B}[ [b] ](\sigma)=\mathrm{F} \\ (\varphi\circ\mathcal{C}[ [c] ])(\sigma) & 若~\mathcal{B}[ [b] ](\sigma)=\mathrm{T} \end{cases}\]

则容易验证 \(\mathcal{C}[ [\mathbf{while}~b~\mathbf{do}~c] ]\) 是 \(F\) 的一个不动点. 因此 \(\mathcal{C}[ [\mathbf{while}~b~\mathbf{do}~c] ]\) 的存在和唯一性可转化为 \(F\) 不动点的存在和唯一性.

事实上，\(F\) 的最小不动点存在且唯一. 这下稳了（

最小不动点的相关讨论

首先需要定义完全偏序集：

Def. 完全偏序集 （例子：离散序 \(a\sqsubseteq b\iff a=b\)，平坦序 \(a\sqsubseteq b\sqsubseteq c \iff a=b~或~b=c\)）

  • 复习一下偏序集：自反、传递、反对称. 偏序集记作 po.
  • 若偏序集中的每个升链 \(d_1\sqsubseteq d_2\sqsubseteq \cdots\) 都有上确界 \(\bigsqcup_{i}d_i\)，则称其为一个完全偏序集，记作 cpo.
  • 若 cpo \((P,\sqsubseteq)\) 中有最小元 \(\perp\)（\(\forall x\in P\)，总有 \(x\sqsubseteq \perp\)），则称其为带底的 cpo.
  • 可以证明：对任意集合 \(X\)，给其幂集赋予包含关系 \((\mathscr{P}(x),\subseteq)\) 都构成一个含底的 cpo.

在 cpo 中，每个升链都有上确界，这实际上就是分析中“极限”的概念. 因此可以定义连续函数：

Def. 连续函数 设 \(D,E\) 是 cpo，\(f:D\to E\) 是一个函数

  1. 若对 \(\forall d_1,d_2\in D\)，s.t. \(d_1\sqsubseteq d_2\)，总有 \(f(d_1)\sqsubseteq f(d_2)\)，则称 \(f\) 单调（保序）；
  2. 若 \(f\) 单调，且对任意升链 \(d_1\sqsubseteq d_2\sqsubseteq\cdots\)，都有 \(f(\bigsqcup d_n)=\bigsqcup f(d_n)\)，则称 \(f\) 连续.

对于连续函数，有如下的不动点定理：

Thm. 不动点定理 设 \(D\) 是一个含底的 cpo，\(f:D\to D\) 连续，则 \[fix(f)=\bigsqcup_n f^n(\perp)\] 是 \(f\) 的最小不动点. 其中 \(f^n\) 表示 \(f\) 作用 \(n\) 次. （证明很简单，先证是不动点，再证最小即可）

现在，我们在状态集 \(\Sigma\) 中添加底元素 \(\perp\)，s.t. \(\forall \sigma\)，\(\perp\sqsubseteq \sigma\). 新的集合记为 \(\Sigma_\perp\).

部分函数当然也可以得到扩充（把无定义的元素全部拉到 \(\perp\) 上）而成为全函数 \(\Sigma\to\Sigma_\perp\). 并且该扩充是一一对应的.

  • 还可以得到：这样扩充得到的全函数一定是连续的.

考虑到部分函数 \(\Sigma\rightharpoonup\Sigma\) 的全体被赋予包含关系后是一个含底的 cpo，一个自然的反应就是：扩充而来的全函数也构成一个含底的 cpo.

事实上，这句话是正确的. \(\Sigma\to\Sigma_\perp\) 上的序构造如下： \[f\sqsubseteq g~当且仅当~\forall\sigma\in\Sigma,~f(\sigma)\sqsubseteq g(\sigma)\]

到这里，就足以说明 while 循环指称语义的存在唯一性了.

关于不动点，在代数上还有如下定理（这里并用不到）：

Thm. Knaster-Tarski 最小不动点定理 设 \((L,\sqsubseteq)\) 是一个完备格. 令 \(f:L\to L\) 是单调函数（不必连续，可以看出这里减弱了条件），则 \[m=\sqcap\{x\in L: f(x)\sqsubseteq x\}\] 是 \(f\) 的最小不动点.

上述定理还有一个逆定理：

Thm. 若所有保序映射 \(f:L\to L\) 都有不动点，则 \(L\) 是完全格.

公理语义

  • 前面的操作语义和指称语义已经对语义有了很详细的描述.
  • 公理语义给出了一套逻辑系统，并证明了其正确性.
  • 这套系统可以被用于自动化推演证明，叫做 Hoare Logic.

断言语言 \(\mathbf{Assn}\)

在算术表达式 \(\mathbf{Aexp}\) 中添加整型变量 \(\mathbf{IntVar}\) 类型的元素（常用 \(i\) 表示），扩充而为 \(\mathbf{Aexpv}\)：

  • \(\mathbf{Aexpv}~a::=X~|~i~|~n~|~a_1+a_2~|~a_1-a_2~|~a_1\times a_2\)

既然有变量，那么就需要有“解释”，记为函数 \(I:\mathbf{IntVar}\to\mathbb{N}\). 这个东西在语义中用得到.

断言（Assertions）就是一些可以判断真假的东西（可视为 \(\mathbf{Bexp}\) 的扩展）：

  • \(\mathbf{Assn}~P::=\mathbf{true}~|~\mathbf{false}~|~a_1<a_2~|~P_1\wedge P_2~|~P_1\vee P_2~|~P_1\Rightarrow P_2~|~\neg P~|~\forall i.~P~|~\exists i.~P\)

由于断言中有变量和量词的出现，因此也有类似数理逻辑中“自由”与“约束”的概念，不多赘述.

\(\mathbf{Assn}\) 的语义：指称语义

  • \(\mathbf{Aexpv}\) 的语义：记为 \(\mathcal{A}v[ [a] ]\)…基本直接套用 \(\mathbf{Aexp}\) 的指称语义. 关于变量的语义如下：\[\mathcal{A}v[ [i] ]I\sigma=I(i)\]
  • \(\mathbf{Assn}\) 的真假：基本与一阶逻辑的东西一样. 用 \(\sigma\vDash_I A\) 表示 \(A\) 在 \(I\) 中被 \(\sigma\in\Sigma\) 满足.
    • 例 1：\(\sigma\vDash_I \mathbf{true}\), \(\sigma\not\vDash_I\mathbf{false}\);
    • 例 2：\(\sigma\vDash_I a_1=a_2\) 当且仅当 \(\mathcal{A}v[ [a_1] ]I\sigma=\mathcal{A}v [[a_2] ]I\sigma\);
    • 例 3：\(\sigma\vDash_I A\wedge B\) 当且仅当 \(\sigma\vDash_I A\) 且 \(\sigma\vDash_I B\).

Prop 给定 \(b\in\mathbf{Bexp}\) 和状态 \(\sigma\in\Sigma\)，则对任意解释 \(I\)，有\[\mathcal{A}[ [b] ]\sigma=\mathbf{true}~当且仅当~\sigma\vDash_I b\]

Hoare 公式（Hoare triple）

Hoare 公式（三元组）一般的形式为 \(\{P\}~c~\{Q\}\)：

  • \(P,Q\in\mathbf{Assn}\) 是断言（描述系统的状态？）；
  • \(c\in\mathbf{Com}\) 是指令.

\(\{P\}~c~\{Q\}\) 的意思是：若 \(P\) 成立，则执行完 \(c\) 后，\(Q\) 将成立.

Hoare Rules

一共有六条规则：

\[ \begin{align*} \mathrm{Skip}~\frac{}{ \{B\} ~\mathbf{skip}~ \{B\} } &\quad \mathrm{Assign}~\frac{} {\{B[a/X]\} ~X:=a~ \{B\} }\\ \mathrm{If}~\frac{ \{A\wedge b\}~c_0~\{B\}\quad \{A\wedge\neg b\}~c_1~\{B\} }{ \{A\}~\mathbf{if}~b~\mathbf{then}~c_0~\mathbf{else}~c_1~\{B\} } &\quad \mathrm{Sequence}~\frac{ \{P\}~c_1~\{R\} \quad \{R\}~c_2~\{Q\} }{ \{P\}~;c_2~\{Q\} } \\ \mathrm{While}~\frac{ \{P\wedge b\}~c~\{P\} }{ \{P\}~\mathbf{while}~b~\mathbf{do}~c~\{P\wedge\neg b\} }&\quad \mathrm{Consequence}~\frac{ \vDash(P\Rightarrow P')\quad \{P'\}~c~\{Q'\}\quad \vDash(Q'\Rightarrow Q) }{ \{P\}~c~\{Q\} } \end{align*} \]

while 循环始终是这些命令中最复杂的. 这里的 \(P\) 叫做循环不变量，在公理语义的讨论中有着很重要的地位.

  • Hoare rules 建立了一套推理系统，进一步可以验证它是可靠的（它推出的结果在语义上都没毛病）.
  • Hoare rules 之间的推理符号用 \(\vdash\).

Hoare 规则的可靠性

Def. 可满足性 \(\sigma\) 在 \(I\) 中满足 \(\{A\}~c~\{B\}\) 当且仅当：若 \(\sigma\vDash_I A\)，则 \(\mathcal{C}[ [c] ]\sigma\vDash_I B\). 记作 \(\sigma\vDash_I \{A\}~c~\{B\}\).

Def. 永真性 若 \(\forall \sigma\)，\(\forall I\)，都有 \(\sigma\vDash_I \{A\}~c~\{B\}\)，则称其是永真的，记作 \(\vDash \{A\}~c~\{B\}\).

Thm. 可靠性 Hoare 规则推理出来的东西都是永真的. i.e. 若 \(\vdash \{A\}~c~\{B\}\)，则 \(\vDash \{A\}~c~\{B\}\).

可靠性的证明需要以下两个引理：

  1. 赋值和语义符号 \([ [ ] ]\) 的交换

Lem. 设 \(a,a'\in\mathbf{Aexpv}\)，\(X\in\mathbf{Loc}\)，则对 \(\forall I\)，\(\forall \sigma\in\Sigma\)，有 \[\mathcal{A} v[ [a[ [a^{\prime} / X] ] I \sigma=\mathcal{A} v[ [a] ] I(\sigma[ [\mathcal{A} v[ [a^{\prime}] ] / X] ])\]

  1. 赋值和 \(\vDash\) 符号的交换

Lem. 设 \(I\) 是一个解释，\(B\in\mathbf{Assn}\)，\(a\in\mathbf{Aexpv}\)，\(X\in\mathbf{Loc}\)，则对 \(\forall \sigma\in\Sigma\)，有 \[\sigma \vDash_{I} B[a / X] ~~\mathrm{iff}~~ \sigma[\mathcal{A}[ [a] ] \sigma / X] \vDash_{I} B\]

引理的证明和定理的证明都不算太困难（while 循环最为困难），不详细描述了…

Hoare 规则的完备性

完备性是指：一个系统能够把所有“正确”的东西都推出来. 这个“正确性”这里有两种解读：

  1. 绝对：\(\{A\}~c~\{B\}\) 真的正确（比如 \(\{x=1\}~\mathbf{skip}~\{x=1\}\)）.
  2. 相对：在断言的逻辑（一阶逻辑）中能证明 \(\vDash\{A\}~c~\{B\}\).
  • 如果按照上述 1. 的定义，则由 Godel 不完备定理可知，Hoare 规则是不完备的.

那么，不完备性从何而来呢？（一方面可考虑 \(\vDash B\) iff \(\{\mathbf{true}\}~\mathbf{skip}~\{B\}\)，另一方面可考虑 \(\{\mathbf{true}\}~c~\{\mathbf{false}\}\)）

实际上，是从 Consequence rule \(\frac{ \vDash(P\Rightarrow P')\quad \{P'\}~c~\{Q'\}\quad \vDash(Q'\Rightarrow Q) }{ \{P\}~c~\{Q\} }\) 中的蕴含（\(\Rightarrow\)）符号来的.

结合 Godel 定理考虑同样可知，Hoare 规则的不完备性应该至少有一部分来自于断言（类似一阶逻辑）的不完备性.

那么，Hoare 规则比断言更加不完备吗？

答案是否定的. 我们称，Hoare 具有相对完备性.

Thm. 相对完备性 Hoare 规则是相对完备的，i.e. 若 \(\vDash \{A\}~c~\{B\}\)，则 \(\vdash \{A\}~c~\{B\}\).

  • 其证明用到了最弱前置条件与可表达性.

先来定义最弱前置条件（Weakest Liberal Preconditions），断言 \(B\) 相对于指令 \(c\) 的最弱前置条件为：

\[wp^{I}[c, B]=\{\sigma \in \Sigma_{\perp}~|~\mathcal{C}[ [c] ] \sigma \vDash^{I} B\}\]

关于上述定义的一点解释：

  • “前置条件”听起来像是一个断言，但是其实是一个状态的集合.
    • 集合 \(S\) 是断言 \(B\) 相对于指令 \(c\) 的前置条件意味着对 \(S\) 中的每个状态执行完 \(c\) 后，\(B\) 都将成立；
    • 最弱前置条件的“最弱”是把上述集合缩到最小，i.e. \(wp^{I}[c, B]\) 是最小的“前置条件”集合.

有了这个定义，可表达性就非常好理解了：

Def. 可表达性 \(\mathbf{Assn}\) 是可表达的，i.e. 对 \(\forall c,B\)，总存在断言 \(A\)，s.t. \(wp^I[c,B]=A^I\) 在 \(\forall I\) 下成立.

  • 其中 \(A^I\) 表示在 \(I\) 下能够使得 \(A\) 成立的状态集.

事实上，上述定义相当直观：最弱前置条件是一个状态集，我们非常难以把它想象成一个“条件”. 但可表达性给出了一个断言 \(A\)，使得断言成立的状态恰好就是这些状态，所以这个最弱前置条件就被断言 \(A\) 所“表达”了.

所有命令的最弱前置条件如下：

\[ \begin{align*} wp[\mathbf{skip}, B] &= B \\ wp[X:=a, B] &= B[a/X] \\ wp[(c_1;~c_2), B] &= wp[c_1, wp[c_2,B] ] \\ wp[\mathbf{if}~b~\mathbf{then}~c_0~\mathbf{else}~c_1,B] &= (b\Rightarrow wp[c_1,B])\wedge (\neg b\Rightarrow wp[c_2,B]) \\ wp[\mathbf{while}~b~\mathbf{do}~c, B] &= \bigwedge_i F_i(B) \\ 其中~ F_0(B)=\mathbf{true},&~F_{i+1}(B)=(\neg b\Rightarrow B)\wedge (b\Rightarrow wp[c, F_i(B)]). \end{align*} \]

然后我们可以得到如下的两条引理：

Lem. 1 \(\forall c\in\mathbf{Com}\)，\(Q\in\mathbf{Assn}\)，有\[\vDash\{wp[c,Q]\}~c~\{Q\}~且~\forall R\in\mathbf{Assn}.~\vDash \{R\}~c~\{Q\}~意味着~(R\Rightarrow wp[c,Q])\]

Lem. 2 \(\forall c\in\mathbf{Com}\)，\(Q\in\mathbf{Assn}\)，有 \(\vdash \{wp[c,Q]\}~c~\{Q\}\).

有了这两条，即可证明相对完备性. 其大致思路是：

  • 对任意命令 \(c\)，断言 \(P\) 和 \(Q\)，s.t. \(\vDash \{P\}~c~\{Q\}\)；
  • 由 Lem 1，有 \(\vDash P\Rightarrow wp[c,Q]\)；
  • 由 Lem 2，有 \(\vdash \{wp[c,Q]\}~c~\{Q\}\)；
  • 由 Consequence rule，可知 \(\vdash \{P\}~c~\{Q\}\).

这里略去了很多细节，具体细节参见 Winskel 的书.