# 荷蘭國旗問題 The Dutch National Flag Problem（中）

``````M ≤ r ≤ w ≤ b ≤ N ∧
(∀i : M ≤ i < r : red(i)) ∧
(∀i : r ≤ i < w : white(i)) ∧
(∀i : b ≤ i < N : blue(i))``````

``````   r, w, b, := M, M, N
{ Inv: M ≤ r ≤ w ≤ b ≤ N ∧ Pr ∧ Pw ∧ Pb, bound: b - w }
; do w < b →
if red(w)   → Sr
| white(w) → Sw
| blue(w)  → Sb
fi
od
{ M ≤ r ≤ w ≤ b ≤ N ∧ Pr ∧ Pw ∧ Pb ∧ b = w }``````

``````Pr ≡ (∀i : M ≤ i < r : red(i))
Pw ≡ (∀i : r ≤ i < w : white(i))
Pb ≡ (∀i : b ≤ i < N : blue(i))``````

`white(w)` 的情形最簡單：把 `w` 遞增之後不變量仍然滿足。`Sw` 可以是 `w := w + 1`.

`blue(w)` 的情況呢？若把 `a[w]``a[b]` 交換，我們可把 `b` 遞減，不變量也剛好滿足。`Sb` 可以是 `swap(b,w); b := b - 1`.

``````  r, w, b, := M, M, N
{ Inv: M ≤ r ≤ w ≤ b ≤ N ∧ Pr ∧ Pw ∧ Pb, bound: b - w }
; do w < b →
if red(w)   → swap(r,w);  r, w := r + 1, w + 1
| white(w) → w := w + 1
| blue(w)  → swap(b,w);  b := b - 1
fi
od
{ M ≤ r ≤ w ≤ b ≤ N ∧ Pr ∧ Pw ∧ Pb ∧ b = w }``````

`red(w)` 的情況為例，我們得證明：

``````  { M ≤ r ≤ w < b ≤ N ∧ Pr ∧ Pw ∧ Pb ∧ red(w) }
swap(r,w)
{ (M ≤ r ≤ w ≤ b ≤ N ∧ Pr ∧ Pw ∧ Pb)[r, w := r + 1, w + 1] }
; r, w := r + 1, w + 1
{ M ≤ r ≤ w ≤ b ≤ N ∧ Pr ∧ Pw ∧ Pb }
``````