🎯 什麼情境該想到我
當你想「嚴謹確認一個迴圈/演算法真的正確」，或迴圈邏輯容易出 off-by-one、難以推理時。
⚙️ 怎麼用（找出並驗證一條在迴圈中恆成立的性質）
- 找不變式：一句在「每次迭代開始前都成立」的陳述（例：排序中「A[0..i-1] 已排好序」）。
- 證三件事：
- 初始化：第一次迭代前，不變式成立。
- 保持：若某次迭代前成立，執行後（下次前）仍成立。
- 終止：迴圈結束時，不變式 + 終止條件 → 推出「演算法正確」。
實務上，即使不寫形式證明，「在腦中維持一條不變式」也能讓你迴圈寫得更對、更少邊界錯誤。
★ 真實例子：Go 標準函式庫的 sort.Search
Go 1.26.4 的 sort/search.go 把不變式直接寫在註解裡：
func Search(n int, f func(int) bool) int {
// Define f(-1) == false and f(n) == true.
// Invariant: f(i-1) == false, f(j) == true.
i, j := 0, n
for i < j {
h := int(uint(i+j) >> 1) // avoid overflow when computing h
// i ≤ h < j
if !f(h) {
i = h + 1 // preserves f(i-1) == false
} else {
j = h // preserves f(j) == true
}
}
// i == j, f(i-1) == false, and f(j) (= f(i)) == true => answer is i.
return i
}逐一對照三個步驟：
| 步驟 | 這裡的證明 |
|---|---|
| 初始化 | i=0、j=n。約定 f(-1)=false、f(n)=true，所以 f(i-1)=false、f(j)=true 成立 |
| 保持 | !f(h) → 設 i=h+1，則 f(i-1)=f(h)=false ✓；f(h) → 設 j=h，則 f(j)=true ✓ |
| 終止 | 每輪 j−i 至少縮小 1（因為 i ≤ h < j），所以一定會停；停時 i==j，不變式給出 f(i-1)=false 且 f(i)=true → i 就是第一個讓 f 為真的位置 |
這段程式碼寫得對的原因，就是每一行賦值都在維持不變式——註解 preserves f(i-1) == false 就是「保持」的證明。
順帶一提 uint(i+j) >> 1：寫成 (i+j)/2 在 i+j 超過 int 範圍時會溢位成負數。這是二分搜尋最有名的 bug——在各種語言的標準函式庫裡潛伏多年才被發現。
★ 用不變式決定邊界：半開區間的好處
二分搜尋的 off-by-one 錯誤，幾乎都來自「沒先想清楚不變式」。先選一種區間語義，再寫程式：
| 語義 | 不變式 | 迴圈條件 | 縮小方式 |
|---|---|---|---|
半開 [i, j) | 答案在 [i, j) 裡 | i < j | i = h+1 或 j = h |
閉區間 [i, j] | 答案在 [i, j] 裡 | i <= j | i = h+1 或 j = h-1 |
混用兩種語義就會出錯（例如用 [i, j) 的初值 j = n，卻用閉區間的 j = h-1）。Go 的 slice 表示法 s[i:j] 本身就是半開區間，所以在 Go 裡一律用半開最自然。
★ 插入排序：教科書的經典例子
《演算法導論》用插入排序介紹迴圈不變式：
for i := 1; i < len(a); i++ {
// 不變式：a[0:i] 是原本 a[0:i] 的元素，且已排序
key := a[i]
j := i - 1
for j >= 0 && a[j] > key {
a[j+1] = a[j]
j--
}
a[j+1] = key
}- 初始化：i=1，a[0:1] 只有一個元素，當然有序。
- 保持：內層迴圈把比 key 大的元素右移一格，把 key 放進正確位置 → a[0:i+1] 有序。
- 終止：i = len(a)，不變式說 a[0:len(a)] 有序 → 整個陣列已排序。
★ 實務用法：把不變式變成斷言
寫不出形式證明也沒關係，把不變式寫成測試時才檢查的斷言：
if debugInvariants && !slices.IsSorted(a[:i]) {
panic(fmt.Sprintf("invariant broken at i=%d", i))
}配合 fuzzing（go test -fuzz）跑大量隨機輸入，不變式一被破壞就會停在第一個出錯的迭代——比在最終結果上除錯快得多。
🧪 我實際套用的紀錄
- 2026-07-15：（待填）
⚠️ 注意
- 不變式要選「強到能推出正確性、又真的每輪都成立」的那條——太弱沒用、太強不成立。
🔗 相關工具
- 工具-遞迴式與主定理 —— 姊妹工具，一個證正確性，一個算複雜度，配成一組看演算法
- 工具-系統化除錯 —— 實務用途，迴圈出 off-by-one 時用不變式定位是哪一輪開始不成立
- 二分搜尋 —— 不變式最常被用到、也最常寫錯的演算法