$BB = (Ej:1 \leq j \leq n : B_{j})$

### 有关选择结构的基本定理

$Q \Rightarrow BB$

$(Aj: 1 \leq j \leq n: (Q \ and \ B_{j}) \Rightarrow wp(SL_{j}, R))$

$Q \Rightarrow wp(IF, R)$

### 有关重复结构的基本定理

$(P \ and \ BB) \Rightarrow wp(IF, R)$

$(P \ and \ wp(DO, T)) \Rightarrow wp(DO, P \ and \ non \ BB)$

### 证明过程

#### 选择结构基本定理证明

$Q \Rightarrow wp(IF, R)$

$wp(IF, R) = BB \ and \ (Aj: 1 \leq j \leq n: B_{j} \Rightarrow wp(SL_{j}, R))$

$A_{1} = (Aj: 1 \leq j \leq n: B_{j} \Rightarrow wp(SL_{j}, R))$

$A_{2} = (Aj: 1 \leq j \leq n: (Q \ and \ B_{j}) \Rightarrow wp(SL_{j}, R))$

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

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

$B_{j} \Rightarrow wp(SL_{j}, R)$

$B_{j} \Rightarrow wp(SL_{j}, R)$

$Q \Rightarrow A_{1}$

$Q \Rightarrow wp(IF, R)$

#### 重复结构基本定理证明

\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}

$wp(DO, P \ and \ non \ BB) = (Ek: 1 \leq k \leq n : H_{k}(P \ and \ non \ BB))$

$(Ek: 1 \leq k \leq n : P \ and \ H_{k}(T)) \Rightarrow (Ek: 1 \leq k \leq n : H_{k}(P \ and \ non \ BB))$

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

\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}

$wp(IF, H_{k-1}(T)) = BB \ and \ (Aj: 1 \leq j \leq n: B_{j} \Rightarrow wp(SL_{j}, H_{k-1}(T)))$

$wp(IF, H_{k-1}(T)) \Rightarrow BB$

$(P \ and \ BB) \Rightarrow wp(IF, P)$

$$\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}$$

\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}

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

### 笔记来源

A Discipline of Programming