“样例能过”只能说明某几条执行路径没有暴露错误。递归算法的证明应拆成两个问题：程序会不会结束，以及结束时返回的是否是正确答案。
第一部分：终止性
THM定理 · 良基递减保证终止
若能为每个调用状态定义一个非负整数规模
例如半开区间 [left,right) 的规模是 right-left。只要子区间严格更短，规模不可能无限下降。快速幂的规模是非负指数，棋盘覆盖的规模是边长或指数 k。
WARN易错点 · 只检查“常见分支”
一个递归函数可能有多个分支。必须证明每个可能执行的递归调用都递减；只要一个边界分支把参数原样传回去，就可能形成无限递归。
第二部分：部分正确性
终止性只保证程序返回，不保证答案正确。递归正确性最自然的证明方法是对规模做数学归纳。
标准证明模板
- 命题：明确规模为
n时函数承诺什么； - 基本情况：证明所有最小规模的返回值正确；
- 归纳假设：假设所有更小合法子问题都正确；
- 归纳步骤：证明当前层的拆分覆盖所有情况，子调用参数合法，Combine 从正确子答案得到正确当前答案；
- 终止性：补充规模严格递减。
IDEA直觉 · 不需要展开无限多层
归纳假设允许你把子调用视为已经履行合同的黑盒。证明的重点因此落在当前层：有没有漏掉情况、重复计数、错误合并或破坏不变量。
完整证明：归并排序
命题 mergeSort(left,right) 返回时，长度为 [left,right) 包含原区间全部元素，且按非递减顺序排列。
基本情况
当
归纳步骤
假设所有长度小于
- 左右两半各自有序；
- 每一半都完整保留自己的原元素。
合并循环每次取两半未处理首元素中的较小者。由两半有序可知，它也是所有未处理元素中的最小者，所以写入后临时数组前缀仍有序。每一步恰好消费一个元素，直到两半全部耗尽，因此既不漏也不重。写回后整个区间有序并保留原多重集合，命题成立。
两个子区间严格短于当前区间，所以递归最终到达
PROP性质 · 正确性包含“排列性”
只证明输出有序还不够。一个程序输出空数组也“有序”，却不是原数组的排序结果。排序证明必须同时维护有序性和元素多重集合不变。
完整证明：快速选择
12E07 · 求第 k 小的数三路划分后得到：
[小于 pivot] [等于 pivot] [大于 pivot]划分不变量保证三段包含原区间全部元素。若 k 位于等于段，答案就是 pivot；若位于左段或右段，另一侧所有元素的相对顺序都不影响第 k 小值，可以只递归目标所在段。
证明时必须说明 k 是全局下标还是子区间内相对秩。本 Lab 使用全局 0-based 下标，递归时保持 k 不变并更新边界。
ANTI反例 · 划分后错误地调整全局 k
若实现使用全局下标，却在进入右段时又减去左段长度，合同发生了静默切换。数组较小时可能碰巧正确，重复值和多层右递归会迅速暴露错误。
计数题要证明“不漏不重”
逆序对等题通常把所有合法数对分成三类：
- 两个下标都在左半；
- 两个下标都在右半；
- 第一个在左半、第二个在右半。
三类互斥且覆盖全部 i<j，左右内部由归纳假设正确统计，Combine 只统计第三类。因此总和不漏不重。
12E14、12E15和12E16的条件不同，但证明骨架相同：先按下标位置分三类，再用有序性证明双指针统计恰好覆盖跨区间合法对。
构造题要证明覆盖与互斥
地毯填补不仅要证明递归终止，还要证明：
- 除真实洞外每个格子恰好被覆盖一次；
- 每块输出确实是合法 L 形骨牌；
- 四个子棋盘的覆盖范围互不重叠；
- 中心骨牌与四个子覆盖合起来没有空缺。
对边长归纳时，中心骨牌让四个象限各有一个洞，归纳假设给出四个合法覆盖；象限互不相交，而中心骨牌占用的三个格在对应子问题中被视为洞，因此不会重复覆盖。
从证明反推测试
证明中的每个前提都可以变成测试类别：
| 证明义务 | 对应测试 |
|---|---|
| 基本情况正确 | 最小规模、空区间或单元素 |
| 分支覆盖完整 | 每个条件分支至少一个输入 |
| 严格比较正确 | 相等值与重复值 |
| 算术不溢出 | 32 位极值、长前缀和、最大计数 |
| 合并不漏不重 | 已排序、逆序、交错、全部相等 |
| 输出顺序稳定 | 多解构造的固定遍历顺序 |
测试不能替代证明，但证明能指出哪些最小反例最有价值。
自检
- “规模为 n 时正确”这一命题为什么必须包含函数的完整输出合同？
- 排序算法只证明相邻元素非递减还缺少什么？
- 对归并计数，为什么跨区间对只在当前层统计一次？
参考答案
- 归纳步骤依赖子调用承诺。若命题只说“返回一个答案”而未说明范围、元素或副作用，当前层无法合法使用归纳假设。
- 还要证明输出恰好是输入元素的一个排列，包括重复元素的重数不变。
- 一对下标第一次被分到左右不同子树的最低公共递归层时被统计；更低层二者在不同子问题中，更高层二者已经位于同一侧，因此不会重复。
下一节把同一棵递归结构用于复杂度分析。