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