# Invariant Guard Correctness

> 当编写或评审"自以为熟悉"的算法（循环/递归/原地修改/边界）时使用；在写代码前先落笔函数契约、循环不变式、终止性论证与边界清单，产出正确性优先的实现与自检；不适用于显然无误的一行式或纯并发同步推理；触发词：循环不变式、二分边界、off-by-one

- Skill: `findscripter/invariant-guard-correctness` (Agent Skill)
- Install (CLI): `npx skillmds@latest add findscripter/invariant-guard-correctness`
- Raw SKILL.md: https://api.skillmd.com/api/skills/findscripter/invariant-guard-correctness/raw
- Safety review: pending
- Works with: Claude Code, Claude.ai, OpenAI Codex
- Category: Coding & Dev Tools
- License: MIT
- Author: findscripter (https://skillmd.com/u/findscripter)
- Updated: 2026-09-17
- Page: https://skillmd.com/skills/findscripter/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 中任一缺失，不得产出代码。**

## 指令

铁律（不可违反）：

```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）、迭代中并发修改。每个适用情形写一句预期行为。
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`。两句不等价——不变式只保证"若存在多数则它是候选"，并不保证"候选是多数"。落笔即见缺口：需要第二趟验证。

```typescript
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`：

```ts
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）。