第六章：狀態機與不變量 — 動畫敘事
第七集 · Ch.6 狀態機與不變量
程式的骨架
每個跑起來的程式，都是一台狀態機。
它有當前的狀態，每次執行一步就轉換到新狀態。
而不變量，是那些在每一步都不會改變的性質——
用它，我們能證明程式永遠不會出錯。
它有當前的狀態，每次執行一步就轉換到新狀態。
而不變量，是那些在每一步都不會改變的性質——
用它，我們能證明程式永遠不會出錯。
狀態機的組成
狀態機（State Machine）由三樣東西定義：
一般狀態
起始狀態
終止狀態（可選）
狀態集合 Q、起始狀態 q₀、轉換關係 δ（delta）
每次「執行一步」就是沿著一條箭頭從一個狀態走到另一個狀態。
每次「執行一步」就是沿著一條箭頭從一個狀態走到另一個狀態。
電梯狀態機 — 互動
狀態：floor=1, door=closed, dir=idle
這個電梯有 4 層樓。觀察狀態如何因每個指令而改變。
電梯不能在門開著的時候移動——這是一個不變量。
電梯不能在門開著的時候移動——這是一個不變量。
不變量的三步驟
要用不變量證明某件事，有標準的三步驟：
定
定義不變量 P(state)
明確說出你認為每一步都會保持的性質。
例：
明確說出你認為每一步都會保持的性質。
例：
(X + Y) mod 3 = 0
基
驗證起始狀態滿足 P
直接代入起始狀態，確認 P 成立。
例：起點 (0,0)：
直接代入起始狀態，確認 P 成立。
例：起點 (0,0)：
(0+0) mod 3 = 0 ✓
保
證明每一步都保持 P
對每種轉換，假設 P(現在狀態) 成立，推導出 P(下一狀態) 也成立。
例：移動 A (+1,+2) 後：
對每種轉換，假設 P(現在狀態) 成立，推導出 P(下一狀態) 也成立。
例：移動 A (+1,+2) 後：
(X+1+Y+2) mod 3 = (X+Y+3) mod 3 = 0 ✓
用
用 P 推導你要的結論
既然 P 永遠成立，任何違反 P 的狀態都永遠無法到達。
例：目標 (1,1)：
既然 P 永遠成立，任何違反 P 的狀態都永遠無法到達。
例：目標 (1,1)：
(1+1) mod 3 = 2 ≠ 0，永遠到不了。
機器人迷宮 — 不變量實戰
不變量：(X + Y) mod 3 = 0 移動 A(+1,+2) 或 B(+2,+1) 後都保持不變
位置：(0,0) 不變量：(0+0) mod 3 = 0 目標 (1,1) 需要 mod = 2
觀念測驗
不變量能用來證明什麼？
小結
1 / 7
本頁為動畫敘事版。看完後可前往
完整第六章
進行互動練習（穩定婚姻演算法、完整機器人迷宮）。
教材來源：Mathematics for Computer Science (Lehman, Leighton, Meyer)