形式语义学学习笔记

这学期上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 的书.