invariant-guard-correctnesslisted

## 何时使用 在编写或评审"显然实现往往悄悄出错"的算法时使用本技能。模型知道什么是循环不变式、递归要有 base case、空表会出问题、`<` 与 `≤` 有别——但它不会在写代码前把这些写下来，于是交付了测试抓不到的细微正确性 bug。 **典型场景（后置条件比循环天然不变式更强）：** - 后置条件强于循环不变式：Boyer–Moore 多数投票、Floyd 判环、最左 vs 任意二分、QuickSelect 划分。 - 读+写双指针的原地修改：原地去重、划分、旋转。 - 带多参数或累加器状态的递归。 - 含重复元素、空输入、边界值的 off-by-one 嫌疑点。 - 必须收敛终止的迭代细化：不动点、牛顿法、EM。 - 任何让你冒出"这算法我会"念头的函数——陷阱通常在契约里，不在循环体里。 **不该用的边界：** - 显然不会失败的一行式：协议本身是开销，留给非平凡的循环/递归/原地修改。 - 纯数学（概率、FFT、几何）：转 `mathguard`，近似算法的后置条件是 ε-界而非等式。 - 并发推理：不变式默认假设单线程；多线程需额外的 happens-before / 可线性化论证，本技能不覆盖。 - 算法尚未选定时：先到 `lemmaly` 定算法，再回来写不变式。 ## 步骤（写代码前的协议，按此顺序） 在产出含循环、递归或非平凡状态的代码前，你的消息必须依次包含： 1. **函数契约** — 前置条件、后置条件、返回值，各一行。 2. **循环不变式** — 每个循环一条（规则 1）。 3. **终止性论证** — 每个循环或递归一条（规则 2、3）。 4. **base case 与度量** — 递归专用（规则 3）。 5. **边界用例表** — 每个适用情形一条，附预期行为（规则 4）。 6. **非法状态不可表示** — 指明用哪些类型或断言来强制不变式（规则 5）。 7. **代码本体。** 8. **自检** — 每个循环一行，确认不变式在循环顶成立、循环体保持它、退出条件蕴含后置条件。 **1–6 中任一缺失，不得产出代码。** ## 指令 铁律（不可违反）： ```text 没有书面的不变式与终止性论证，就不写任何循环或递归 ``` 若你无法用一句话写出不变式，说明你还没设计好这个循环。 **五条不可协商规则：** 1. **每个循环一行不变式。** 写循环前，一句话陈述每次迭代顶部成立的事实。例：`循环顶：result 等于 a[0..i) 之和`；`循环顶：lo ≤ 目标位置 ≤ hi`。 2. **每个循环一行终止性论证。** 指名每次迭代严格递减（或严格趋向某界）的量。例：`hi − lo 每次严格递减`；`i 每次 +1 且以 n 为上界`。无终止性论证则不写循环。 3. **每个递归显式给出 base case 与度量。** 写出 base case（不再递归的最小输入）、度量（每次递归调用严格递减的非负整数，如 `len(xs)`、`hi − lo`、`depth`）、组合方式（子结果如何合成答案）。互递归：陈述跨整个环的度量。 4. **写代码前列边界，不是写完后。** 对集合/数值函数，列出适用项及其行为：空输入（`[]`/`""`/`null`/`None`）、单元素、全相等、已排序/逆序、重复（当假设唯一时）、负数/零/恰为边界值、整数上下溢、NaN/±Inf/`-0`/非规格化浮点、off-by-one 边界（索引 0、n−1、n，长度 0、1）、迭代中并