🎯 什麼情境該想到我
當你想「嚴謹確認一個迴圈/演算法真的正確」，或迴圈邏輯容易出 off-by-one、難以推理時。
⚙️ 怎麼用（找出並驗證一條在迴圈中恆成立的性質）
- 找不變式：一句在「每次迭代開始前都成立」的陳述（例：排序中「A[0..i-1] 已排好序」）。
- 證三件事：
- 初始化：第一次迭代前，不變式成立。
- 保持：若某次迭代前成立，執行後（下次前）仍成立。
- 終止：迴圈結束時，不變式 + 終止條件 → 推出「演算法正確」。
實務上，即使不寫形式證明，「在腦中維持一條不變式」也能讓你迴圈寫得更對、更少邊界錯誤。
🧪 我實際套用的紀錄
- 2026-07-15：（待填）
⚠️ 注意
- 不變式要選「強到能推出正確性、又真的每輪都成立」的那條——太弱沒用、太強不成立。
🔗 相關工具
- 工具-遞迴式與主定理 —— 姊妹工具，一個證正確性，一個算複雜度，配成一組看演算法
- 工具-系統化除錯 —— 實務用途，迴圈出 off-by-one 時用不變式定位是哪一輪開始不成立