1.3 如何验证正确性
学习目标
学完这一节，你能：
- 区分"测试通过"和"算法正确"这两件事
- 用反例快速推翻一个看似合理的算法
- 用循环不变式审查带循环的代码为什么正确
- 让 AI 参与验证，但不把正确性判断交给 AI
- 把验证过程写成一份可追溯的推理收据
能跑，不等于正确
当你让 coding agent 写代码时，它经常会给出一段看起来很完整的实现：函数名合理，注释清楚，测试样例也能通过。
这很容易让人放松警惕。
但算法错误常常不是语法错误。语法错误会报错，算法错误可能只是悄悄返回一个错误答案。更麻烦的是，它可能只在某个边界情况下出错，而你的测试刚好没有覆盖那个情况。
假设你让 AI 写一个函数：
给定若干会议的开始和结束时间，判断一个人能否参加所有会议。
AI 给出思路：
先按开始时间排序。然后检查每个会议的开始时间是否大于前一个会议的结束时间。如果都大于，就可以参加所有会议。
这听起来很合理。但请先停一下。
如果一个会议 10:00 结束，下一个会议 10:00 开始，算冲突吗？
如果不算冲突，那么 AI 的"大于"就是错的，应该允许"大于等于"。一个很小的边界约定，就能改变代码是否正确。
所以，正确性验证的第一步不是跑代码，而是回到问题规格：什么答案才算对？
正确性审查的四层
审查一段 AI 生成的算法，可以按四层进行。
| 层次 | 要问的问题 | 产出 |
|---|---|---|
| 规格 | 它解决的是原问题吗？ | 输入、输出、边界约定 |
| 反例 | 有没有一个输入能让它失败？ | 失败用例和错误原因 |
| 证明 | 为什么它对所有合法输入都成立？ | 不变式、归纳或交换论证 |
| 收据 | 我为什么接受、修改或拒绝它？ | 推理收据 |
这四层不是形式主义。它们分别防止四类常见错误：
- 规格错：代码解决了另一个问题
- 边界漏：常规样例通过，特殊输入失败
- 逻辑跳：算法看起来合理，但没有证明
- 责任丢失：你接受了 AI 的答案，却说不清为什么
第一层：先确认规格
验证正确性之前，先写一份小规格。
以会议问题为例：
输入：若干区间 [start, end]，start 和 end 是时间戳
输出：如果任意两个会议都不重叠，返回 true；否则返回 false
边界约定：
- 空列表返回 true
- 单个会议返回 true
- 如果一个会议结束时间等于下一个会议开始时间，不算冲突
- 非法区间 start > end 需要提前拒绝这份规格会立刻改变你对代码的判断。
如果代码使用 next.start > prev.end，它会把 [9, 10] 和 [10, 11] 判断为冲突。按照上面的规格，这是错的。
如果你的业务规定"两个会议之间必须至少留 5 分钟"，那同一段代码又可能不够严格。
同一个算法动作，在不同规格下可能对，也可能错。AI 不知道你的真实规格，除非你写出来。
与 AI 协作
不要直接问：
这段代码对吗？
更好的问法是：
下面是问题规格和代码。请先检查代码是否完整满足规格；如果不满足，请给出最小反例。不要先重写代码。
这样，AI 的任务从"安慰你代码没问题"变成了"按规格找问题"。
第二层：用反例找错
反例是证明算法错误的最快方式。你只需要找到一个合法输入，让算法输出错误答案。
反例的力量在于：它不和算法争辩，只让算法失败。
还是会议问题。如果 AI 使用了严格大于号：
def can_attend_all(meetings):
meetings.sort()
for i in range(1, len(meetings)):
if meetings[i][0] <= meetings[i - 1][1]:
return False
return True按照"结束时间等于开始时间不冲突"的规格，最小反例是：
meetings = [(9, 10), (10, 11)]这两个会议可以连续参加，正确答案应该是 True。但代码返回 False。
有了这个反例，你不需要再说"我感觉这里不对"。你可以明确指出：代码违反了边界约定。
反例从哪里来
构造反例不是靠运气。你可以按几种固定模式试。
| 模式 | 适合找什么错误 | 例子 |
|---|---|---|
| 最小输入 | 初始化和空输入错误 | 空数组、单元素、只有一个会议 |
| 刚好相等 | < 和 <= 的边界错误 | 结束时间等于开始时间 |
| 重复元素 | 去重、计数、稳定性错误 | 全部元素相同 |
| 极端顺序 | 排序退化、递归调用过深 | 已排序、逆序、接近有序 |
| 局部规则陷阱 | 只看眼前最好的选择，忽略整体结果 | 先选最贵商品，反而花不满预算 |
只看眼前最好的规则，尤其需要反例压力测试。
例如，你有 10 元预算，必须从下面三件商品中选两件，目标是在不超过预算的前提下让总价尽可能高：
| 商品 | 价格 |
|---|---|
| A | 8 |
| B | 6 |
| C | 4 |
如果策略是"先选最贵的商品，再选一个还能放进预算的最贵商品"，它会先选 A，剩余预算 2，无法再选第二件商品。这个策略失败了。
但更好的选择是 B 和 C，总价正好 10。
这个反例说明：局部看起来最好的选择，不一定导向整体最好的结果。你不能因为 AI 给出一个"每一步都选当前最好"的规则，就直接接受它。你要问它：这个局部规则为什么不会破坏最终目标？
第三层：用循环不变式证明对
反例能证明错，但不能证明对。
如果你试了很多反例都没发现问题，只能说明"暂时没找到错"。要说明一个循环算法为什么对，你需要一个更强的工具：循环不变式。
循环不变式是在循环每次迭代前后都保持为真的性质。证明一个不变式通常分三步：
- 初始化：循环开始前，不变式成立。
- 保持：如果某次迭代前不变式成立，执行一次循环后仍成立。
- 终止：循环结束时，不变式能推出我们想要的结果。
这其实是归纳法在程序上的应用。
例子：审查一个排序实现
AI 给出下面这段代码：
def sort(arr):
n = len(arr)
for i in range(n):
for j in range(i + 1, n):
if arr[i] > arr[j]:
arr[i], arr[j] = arr[j], arr[i]
return arr它能通过很多测试。但它为什么正确？
外层循环可以用这个不变式审查：
在每次外层循环开始时，
arr[0:i]已经包含原数组中最小的i个元素，并且按升序排列。
现在检查三步：
初始化：当 i = 0 时，arr[0:0] 是空区间。空区间当然已经有序，也包含最小的 0 个元素。
保持：假设某次循环开始时，arr[0:i] 已经放好了最小的 i 个元素。内层循环会把 arr[i] 和后面所有更小的元素交换。循环结束后，arr[i] 就是剩余元素中的最小值。因此 arr[0:i+1] 包含最小的 i+1 个元素，并且有序。
终止：当外层循环结束时，i = n。根据不变式，arr[0:n] 包含最小的 n 个元素，并且有序。整个数组排序完成。
这段证明不只是为老师看的。它会帮你发现代码中的关键点：内层循环为什么要从 i + 1 开始？交换条件为什么是 arr[i] > arr[j]？外层循环每次到底确认了什么？
如果 AI 写不出这样的不变式，它可能只是生成了熟悉的代码形状，而没有真正解释正确性。
测试、反例和证明的分工
测试很重要，但测试不是全部。
| 方法 | 能证明什么 | 不能证明什么 |
|---|---|---|
| 测试 | 某些输入上行为正确，或发现具体错误 | 所有输入都正确 |
| 反例 | 一个算法是错的 | 一个算法是对的 |
| 不变式 | 一类循环算法为什么正确 | 规格是否选对、复杂度是否可接受 |
这三者应该配合使用。
你可以先用测试快速发现明显错误，再用反例攻击边界和策略，再用不变式说明关键循环为什么对。
在 agent 时代，还要加上第四件事：把你的判断留下来。
第四层：写正确性推理收据
当你审查 AI 代码时，最后不要只提交"修改后的代码"。你要提交一份正确性推理收据。
可以用这个模板：
问题规格：
- 输入：
- 输出：
- 边界约定：
我的预测锁：
- 我认为最容易错的地方：
- 我准备重点测试的反例：
- 我认为需要证明的循环或递归：
AI 输出摘要：
- 算法思路：
- 关键代码：
正确性审查：
- 我构造的反例：
- 反例结果：
- 是否需要修改：
- 关键不变式：
- 初始化 / 保持 / 终止是否成立：
我的决策：
- 接受 / 修改 / 拒绝：
- 理由：
- 仍然不确定的地方：推理收据的重点不是让文档变厚，而是让你的判断可审查。
如果以后线上出错，你能回头看到当时为什么接受这段代码。是规格写错了？反例没覆盖？不变式其实没有证明终止？还是 AI 的解释被你无条件继承了？
AI 可以帮什么，不能替你做什么
AI 很适合参与正确性验证，但要给它正确的角色。
| 任务 | AI 可以做 | 人必须判断 |
|---|---|---|
| 规格审查 | 找歧义、补边界问题 | 哪个边界约定符合真实需求 |
| 反例构造 | 批量生成边界用例 | 哪些反例真正击中问题 |
| 不变式草稿 | 提出可能的不变式 | 不变式是否足够强、三步是否成立 |
| 测试生成 | 写单元测试和性质测试 | 测试是否覆盖关键风险 |
| 代码修复 | 按反例修改实现 | 修改是否改变了原问题 |
最危险的问法是：
这段代码有没有问题？
这个问题太宽，AI 很容易给出一段听起来合理的安慰。
更好的问法是：
请根据下面的规格，给出三个最小反例，尝试推翻这段算法。如果找不到反例，请写出循环不变式，并逐步检查初始化、保持和终止。
你不是让 AI 当裁判。你是让它当审查助手。
本节要点
- 能跑不等于正确；测试通过也不等于所有输入都正确。
- 正确性验证先从规格开始，规格不清，验证没有对象。
- 反例用来证明错误，尤其适合审查 AI 给出的局部规则、边界处理和特殊假设。
- 循环不变式用来证明带循环的算法为什么正确。
- AI 可以帮助生成反例、测试和不变式草稿，但人要承担最终判断。
- 高质量提交不只包含代码，还应包含正确性推理收据。
课堂练习
练习 1：会议安排的最小反例
下面是 AI 给出的代码：
def can_attend_all(meetings):
meetings.sort()
for i in range(1, len(meetings)):
if meetings[i][0] <= meetings[i - 1][1]:
return False
return True假设业务规定：一个会议结束时间等于下一个会议开始时间，不算冲突。
请完成：
- 写出这个问题的输入、输出和边界约定。
- 给出一个最小反例。
- 修改代码中的判断条件。
- 写一句话说明你为什么接受修改后的代码。
练习 2：为排序代码写不变式
针对本节的 sort(arr) 代码，写出外层循环的不变式，并检查：
- 初始化是否成立？
- 保持是否成立？
- 终止时能否推出整个数组有序？
- 这个算法是否稳定？如果不稳定，给出一个说明。
练习 3：审查 AI 的局部规则
让 AI 回答：
有 10 元预算，必须从价格为 8、6、4 的三件商品中选两件，让总价尽可能高但不超过预算。能不能总是先选最贵的商品？
然后提交一份推理收据：
- 你的预测锁：你认为这个规则是否正确？
- AI 的回答摘要
- 你构造的反例
- 你最终接受、修改或拒绝 AI 建议的理由
评分重点不是你是否一开始就答对，而是你是否能用反例或证明支撑自己的最终判断。
课后测验
📝 课后测验
上一节：1.2 六问诊断法
下一节：1.4 复杂度判断