Invariant guard correctness

何时使用

在编写或评审"显然实现往往悄悄出错"的算法时使用本技能。模型知道什么是循环不变式、递归要有 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 中任一缺失，不得产出代码。

指令

铁律（不可违反）：

没有书面的不变式与终止性论证，就不写任何循环或递归

若你无法用一句话写出不变式，说明你还没设计好这个循环。

五条不可协商规则：

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）、迭代中并发修改。每个适用情形写一句预期行为。
5. 让非法状态不可达，而非仅不处理。 优先把约束编码进类型与结构：用和类型替代布尔标志糊（Loading | Loaded(data) | Error(msg) 而非 {loading, data, error}）；用 newtype 防 ID 混淆（UserId vs OrderId）；需至少一个元素时用非空列表类型；在边界处解析而非下游反复校验（parse-don't-validate）。语言表达不了时，把不变式写成注释并在边界断言。

产出纪律： 每个循环带一行 // inv:（或 # inv:）注释陈述不变式；每个递归注释写明 base case 与度量；处理步骤 5 中列出的每个边界，或显式委派（"空输入抛错——调用方责任"）；廉价时在入口断言前置条件；语言允许处优先用类型（和类型、newtype、非空、非 null）替代运行时检查。

示例

陷阱：Boyer–Moore 多数投票——"陷阱在契约里，不在循环体里"的典范。

不带本技能交付的实现，在 [1,2,3]（返回 3，应为 null）和 [2,2,1,1]（返回 1，应为 null）上失败。投票循环是对的，错的是后置条件。协议如何抓住它：

写**步骤 1（契约）逼出后置条件：当且仅当 count(x, arr) > arr.length/2 时返回 x，否则 null。写步骤 2（循环不变式）**逼出：若 arr 存在严格多数元素，则循环退出时它等于 candidate。两句不等价——不变式只保证"若存在多数则它是候选"，并不保证"候选是多数"。落笔即见缺口：需要第二趟验证。

function findMajority(arr: number[]): number | null {
  if (arr.length === 0) return null;
  // Pass 1: 投票
  let candidate = arr[0], count = 0;
  // inv: 若 arr 存在严格多数，则在每个 count===0 重置点它等于 candidate
  for (const x of arr) {
    if (count === 0) candidate = x;
    if (x === candidate) count++; else count--;
  }
  // Pass 2: 验证——投票不变式严格弱于后置条件
  let tally = 0;
  // inv: tally = candidate 在 arr[0..i) 中的出现次数
  for (const x of arr) if (x === candidate) tally++;
  return tally * 2 > arr.length ? candidate : null;
}

同一陷阱推广到：Floyd 判环（找到相遇点只证明有环，不给环起点，需第二趟走）；双指针"找任意" vs "找最左"（一者的不变式不满足另一者的后置条件）；QuickSelect 划分（划分不变式 off-by-one 会悄悄破坏"该位置是第 k 小"）；DP 重构（表给最优值，重构最优路径需对选择数组另立不变式）。规则：先写后置条件，再写循环不变式，检查后者蕴含前者；不蕴含就是缺一趟、缺一查或缺辅助状态。

范例：二分查找最左匹配。 多数"我会二分"的实现是为"找任意匹配"写的，陷阱在后置条件。给定含重复的升序数组，返回 target 最左出现的下标，否则 -1：

function leftmost(a: number[], target: number): number {
  // contract:
  //   pre:  a 升序
  //   post: 返回最小的 i 使 a[i] === target，缺失则 -1
  let lo = 0, hi = a.length;                 // 半开区间 [lo, hi)
  // inv: 所有 < lo 的下标 a[i] < target；所有 ≥ hi 的下标 a[i] > target 或已越过最左匹配
  // term: hi - lo 每次严格折半
  while (lo < hi) {
    const mid = (lo + hi) >> 1;
    if (a[mid] < target) lo = mid + 1; else hi = mid;
  }
  // exit: lo === hi，由不变式 lo 是 a[lo] >= target 的最左下标
  return lo < a.length && a[lo] === target ? lo : -1;
}

循环形状不变，差别是契约先写——循环体被选成维持一个"蕴含后置条件"的不变式。注意不能在命中时早返回（那只给任意匹配）。

常用不变式模式（速查）：

循环/算法形状	典型不变式	终止性
线性扫描累加	顶部 acc = f(a[0..i))	i +1，以 n 为界
双指针（有序）	目标（若有）落在 a[lo..hi]	hi − lo 严格递减
二分查找	目标（若在）∈ a[lo..hi] 且非空	hi − lo 严格折半
滑动窗口	窗口 [l..r) 满足约束；答案 ≥ 目前最优	r 每轮至少前进一次
BFS	距离 <d 的节点已弹出；队列含距离 d 的节点	每次弹出节点数严格减
原地划分	a[0..i) < pivot；a[i..j) ≥ pivot；a[j..n) 未见	n − j 严格递减

注意事项

• 不是自动证明器。 本技能要求作者"写"不变式，不会机械检验；配合基于属性的测试（property-based）取得更强证据。
• 默认不含并发。 所述不变式假设单线程，除非显式扩展；多线程需额外 happens-before/可线性化论证。
• 浮点与溢出边界依赖语言。 边界表是清单，不替代你对所在语言数值语义的理解。
• 会拖慢平凡代码。 一眼无误的一行式上，协议是纯开销。
• 唯一的强制手段是文档。 作者跳过写不变式，本技能无法检测——配合代码评审或要求填契约的 PR 模板。

警惕这些借口："这算法我会，单趟搞定"（知道循环 ≠ 知道契约，陷阱在循环不强制的后置条件里）；"我脑内跑过，没问题"（心算跳过边界，写下不变式并验证它蕴含后置条件）；"边界显然"（那就花 30 秒写下来）；"测试会抓到"（测试只抓你想到的例子，后置条件抓所有例子）；"加验证趟显得冗余"（Boyer–Moore 投票+验证仍是 O(n)，"显得冗余"正是交付 bug 的借口）。

红旗——停下先写不变式：将写 while(...) 却没陈述进入时成立的事实；将写 if (i === n−1) 或 if (i === n)；将递归却没在本消息命名 base case；将写 // TODO: handle empty；将对浮点用 ==；将在循环中途静默吞掉错误。

验证清单（声称正确前逐项核对）： 每个循环有一行 // inv:；每个循环有书面终止性论证；每个递归命名 base case 与度量；函数后置条件已写且被最后循环的退出状态蕴含；表中每个适用边界有测试或显式"委派给调用方"说明；至少一个测试覆盖每个非平凡边界（空、单元素、最大值、off-by-one）；被拒的非法状态要么类型上不可表示、要么入口断言；近似/随机算法的 ε-界写进后置条件而非等式。不能逐项打勾，则代码是"例子正确"而非"行为正确"——补缺口或降级所声称的契约。

一句话主旨：测试验证例子，不变式验证行为；AI 默认交付"例子正确、行为错误"的代码，本技能让它先就行为推理。

互见

• lemmaly — 写不变式前算法选型须先定；算法族不清时先用它。
• mathguard — 近似/随机算法的 ε-界后置条件。
• complexity-cuts — 若 3+ 次优化变换都测试失败，bug 是缺契约而非缺优化，升级到此。

---

采编自 sickn33/antigravity-awesome-skills（MIT）。