本书第五章要推导两个定理,一个是关于\( if-fi \)结构的,一个是关于\( do-od \)结构的。令

有关选择结构的基本定理

令,有选择结构IF和一对谓词\(Q\)和\( R \),使得

对所有的状态都有:

那么,对所有的状态均有

有关重复结构的基本定理

令选择结构 \( IF \) 和一个谓词 \( P \) 在所有的状态下都有

那么,对于相应的重复结构 \( DO \),我们有

这个定理也被称为“循环的基本不变式定理”(Fundamental Invariance Theorem for Loops),其直观意义可以理解为:

如果初始状态使得 \( P \) 成立且存在 guard \( B_{j} \)为真, 那么在执行相应的 statement lists 之后,这些初始状态将使系统终止于一个满足 \( P \) 的最终状态。如果上述条件成立,那么将有, 使得 \( P \) 成立且使得循环完美终止的初始状态,在整个循环结构完成时,将使系统终止于一个满足 \( P \) 且不存在 guard \( B_{j} \)为真的最终状态。

证明过程

选择结构基本定理证明

要证

已知:

以及

因为 \( Q \Rightarrow BB \),所以要证明定理成立,只需证明 \( Q \Rightarrow A_{1} \)即可。

将状态空间分为两个互不相交的集合,分别记为 \(Q_{f}\) 和 \(Q_{t}\),分别表示使 \(Q\) 为 false 的初始状态的集合和使 \( Q \) 为 true 的初始状态集合,其中 \(Q_{t} = Q\)。

\(Q_{f}\) 中的初始状态,因为 \(Q\) 为 false,所以 \( Q \Rightarrow A_{1} \)恒成立。

\( \forall p \in Q\),使得 \( B_{j} \) 为 true 或者 false。对于在 \( p \) 上为 false 的 \( B_{j} \),有

即 \( p \) 满足条件 \( A_{1} \)。

对于在 \( p \) 上为 true 的 \( B_{j} \),有 \( p \in B_{j} \),结合条件 \( A_{2} \),有 \( p \in wp(SL_{j}, R) \)。因此,\( \forall p \) 使得 \( B_{j} \) 为真,都有 \( wp(SL_{j}, R) \) 为真,即

即 \( p \) 满足条件 \( A_{1} \)。

综上,\( \forall p \in Q\),\( p \) 满足条件 \( A_{1} \),即

因此,对所有的状态均有

重复结构基本定理证明

要证明

\begin{align} (P \ and \ wp(DO, T)) \Rightarrow wp(DO, P \ and \ non \ BB) \label{origin} \end{align}

已知:

\begin{split} P \ and \ wp(DO, T) & = P \ and \ (Ek: 1 \leq k \leq n : H_{k}(T)) \\ & = (Ek: 1 \leq k \leq n : P \ and \ H_{k}(T)) \end{split}

以及:

因此,式子 \eqref{origin} 等价于

因此,要证明式子 \eqref{origin},只需证明以下式子即可:

\begin{align} P \ and \ H_{k}(T) \Rightarrow H_{k}(P \ and \ non \ BB) \label{key} \end{align}

当 \( k = 0 \) 时,因为

\begin{split} P \ and \ H_{0}(T) = P \ and \ non \ BB = H_{0}(P \ and \ non \ BB) \end{split}

得到

\begin{align} P \ and \ H_{0}(T) \Rightarrow H_{0}(P \ and \ non \ BB) \label{zero} \end{align}

当 \( k > 0 \) 时,因为

得到

又因为

因此,\eqref{key} 式左边有

\begin{equation} \begin{split} P \ and \ H_{k}(T) & = P \ and \ [wp(IF, H_{k-1}(T)) \ or \ non \ BB] \\ & = [P \ and \ wp(IF, H_{k-1}(T))] \ or \ [P \ and \ non \ BB] \\ & \Rightarrow [P \ and \ BB \ and \ wp(IF, H_{k-1}(T))] \ or \ [P \ and \ non \ BB] \\ & \Rightarrow [wp(IF, P) \ and \ wp(IF, H_{k-1}(T))] \ or \ [P \ and \ non \ BB] \\ & = [wp(IF, P \ and \ H_{k-1}(T))] \ or \ [P \ and \ non \ BB] \end{split} \label{key-leftside} \end{equation}

\eqref{key} 式右边有

\begin{align} H_{k}(P \ and \ non \ BB) = wp(IF, H_{k-1}(P \ and \ non \ BB)) \ or (P \ and \ non \ BB) \label{key-rightside} \end{align}

综合式子 \eqref{key-leftside} 以及式子 \eqref{key-rightside},要证明式子 \eqref{key},只需证明:

\begin{align} P \ and \ H_{k-1}(T) \Rightarrow H_{k-1}(P \ and \ non \ BB) \label{k-1} \end{align}

用数学归纳法证明。由上述论证可知:当 \( k = 0 \) 时,\eqref{zero} 成立;\( \forall k > 0 \),当 \eqref{k-1} 成立时,有 \eqref{key} 成立。

综上,当 \( k \geq 0 \) 时, \eqref{key} 成立。由此,\eqref{origin} 得证。

笔记来源

A Discipline of Programming