二分查找在长度为 1 的数组上出错，通常不是“特殊情况太多”，而是区间含义没有统一。若把循环中的每个变量解释成一个持续成立的命题，空数组、重复值和目标缺失就能进入同一个证明。

第 00 篇定义了输入输出契约。本篇把契约连接到代码：先证明允许重复值的左边界二分，再用结构归纳证明树上聚合。输入均为有限数据，操作期间不被其他线程修改。一般性证明写在正文；有限检查由 examples/advanced-algorithms/check_foundations.py 运行。

二分查找返回的是边界

给定非降序整数数组 A，长度为 n，以及整数 x，返回最小下标 p，使得 A[p] 不小于 x。没有这样的元素时返回 n。等价地，输出要满足：

0≤p≤n,∀i<p, A[i]<x,∀i≥p, A[i]≥x.0\le p\le n,\qquad \forall i<p,\ A[i]<x,\qquad \forall i\ge p,\ A[i]\ge x.

最后一个量词仅针对数组合法下标。数组为空时 p=0，两个全称命题都因没有反例而成立。返回的是可插入位置，并不承诺那里恰好等于 x。这与 Python bisect_left 的分区语义一致。Python 文档

使用半开候选区间 [lo,hi)，初值 lo=0, hi=n。每轮取 mid=(lo+hi)//2；若 A[mid]<x，令 lo=mid+1，否则令 hi=mid。当 lo=hi 时返回 lo。这里未调用切片，所以每轮没有隐含的数组复制。

四项证明义务

循环不变量描述每次检查循环条件时都成立的事实，不是对“程序大致在做什么”的摘要。Cornell 的讲义把建立、保持、退出结论和终止分别处理；缺少终止性时，只能得到“如果程序结束，结果正确”的部分正确性。Cornell Loop invariants

这里的不变量为：0≤lo≤hi≤n0\le lo\le hi\le n；下标小于 lo 的元素严格小于 x；下标不小于 hi 的元素不小于 x。尚未分类的元素处于 [lo,hi)。Cornell 的半开区间讲义也用左侧 <v、右侧 >=v 的形式表达此类搜索。Cornell CS2110 Lecture 4

初始化时，两侧已分类区间都为空，数组边界关系显然成立。若 A[mid]<x，由非降序性可知从 lo 到 mid 的元素都小于 x，因此把 lo 移到 mid+1 不会丢掉正确边界。若 A[mid]>=x，从 mid 到原 hi 之前的元素都不小于 x，把 hi 改为 mid 同样保持命题。

循环退出时 lo=hi，未知区间为空。左侧严格小于 x，右侧不小于 x，恰好就是输出 p 的定义。该论证同时覆盖缺失目标：例如 [1,3] 查 2 返回 1，而不是返回一个“未找到”的哨兵。

终止性用非负整数 hi−lohi-lo。当区间非空，mid 落在 [lo,hi)；无论进入哪个分支，新区间长度都严格减小。非负整数不能无限严格下降，所以循环结束。需要强调“严格”：若小于分支写成 lo=mid，数组 [1] 查 2 时 lo 永远为 0。

证明中的有序性不可删除。对于 [3,1] 查 2，按同样代码可能返回 n，却遗漏下标 0。代码没有每次验证输入是否有序，因为那会先花 O(n) 时间；有序性是调用者必须满足的前提。

重复值暴露契约差异

数组 [1,1,3] 查 1，左边界必须为 0。第一次 mid=1，A[mid]=1，正确分支把 hi 改为 1；第二次 mid=0，再把 hi 改为 0。若把判断写成 A[mid]<=x，程序寻找的是右边界，结果变为 2。

把反例缩小到 [0] 查 0，正确答案为 0，错误版本返回 1。这个反例足以否定“两个比较符号可以互换”的命题，却不能证明修复后的所有输入都正确。证明仍依赖前面的不变量与下降量。

在整数比较与数组随机访问均为单位成本的模型下，每轮未知区间至多约减半，循环次数为 O(log(n+1))，额外空间 O(1)。若一个数含 L 位，比较代价还需乘入相应位复杂度；这不改变区间缩小的次数。上述界是最坏界，没有随机变量或操作序列平均。

树上聚合的归纳对象

榜单后续会需要子树大小，区间查询还会需要值的和。教学模块 tree_aggregate.py 的节点为 Node(value,left,right)，value 是整数，允许负数。输入树有限、无环，左右子树没有共享节点。若允许共享，那就是 DAG，递归可能重复计数，必须重新定义需求。

aggregate(root) 返回二元组 (节点数, 值之和)。空树返回 (0,0)；非空树分别计算左右结果，再返回 (1+左节点数+右节点数, value+左和+右和)。输入规模 n 表示节点数，总和记为 S，二者不能混淆。

结构归纳的基础情形是空树，返回 (0,0) 符合定义。归纳假设是左右子树调用分别返回准确节点数与总和。左右子树及根的节点集合互不相交，把三个部分相加恰好得到整棵树的结果。每次递归进入真子树，有限树的节点数严格减少，所以函数终止。

这个归纳步骤不依赖左右子树形状，因而覆盖任意有限合法树，包括只有左孩子的链。程序检查另外用显式栈遍历全部节点，分别计数、累加 value，作为控制流独立的参照。对根值 2、左孩子 -1、右孩子 4、右孩子的左孩子 4，结果应为 (4,9)。

正确性成立，性能前提仍可失效

树上聚合访问每个节点一次，在单位成本加法模型下时间为 Θ(n)。递归额外栈空间为 O(h)，h 是树高：平衡树为 O(log n)，链为 O(n)。不能因为程序写成“左右各递归一次”，就把 h 当成 log n。

Python 递归还有解释器栈深限制。数学上的有限递归一定终止，不保证深链在具体进程里不会触发 RecursionError。教学检查使用小树；大规模不平衡树应采用显式栈或者保证高度的结构。若中间总和有很大位长，加法成本也要进入分析，不能把任意精度加法隐藏在 Θ(n) 的单位模型里。

第 06 篇允许一个节点保存重复键数量 count 时，记录总数的公式变为 count + 左记录数 + 右记录数。若把结果缓存在节点中，还要增加表示不变量：缓存始终等于这个表达式。只证明聚合公式还不够，还必须证明旋转、插入和删除都重新计算了受影响节点。当前结构归纳与独立遍历方法可以复用，但必须明确计的是节点还是记录。

可复跑检查与练习

1
python3 examples/advanced-algorithms/check_foundations.py

检查将小范围非降序数组与标准库 bisect_left 对照，包含空数组、重复值、左右越界目标，并运行故意错误版本寻找反例。树的递归汇总另与迭代遍历对照。实际范围与结果保存在 examples/advanced-algorithms/results/foundations.json；这些属于教学实现验证，不是对无穷输入空间的机器证明。

本篇检查契约列出证明与测试的对应点。由退出条件倒推不变量是一种可迁移方法：先写“返回值必须把输入分成哪两部分”，再安排变量恰好描述这两部分；不要从记忆中的 while 模板猜边界。

  1. 证明右边界二分：返回第一个严格大于 x 的位置。写出两侧不等式、每个分支和下降量；用 [1,1,3] 查 1 手算。指出它与本篇故意错误版本何时反而是同一个正确算法。
  2. 将树节点扩展为保存正整数 count，聚合同时返回节点数与记录总数。写出结构归纳，再用显式栈参照检查一条链和一棵含重复 count 的树。解释为什么两棵子树共享一个节点时，原证明不能直接复用。

参考资料