请求证明此二分查找算法框架的正确性
2026-8-15
二分查找框架正确性证明
这个模板是专门用来寻找搜索空间中第一个满足条件的元素的二分查找实现，核心是通过不断缩小有效搜索区间，最终定位到目标。下面用循环不变式严格证明它的正确性：
前提假设
要让这个模板生效，必须满足两个核心条件：
- 搜索空间是有序的（二分查找的基础，无序空间无法用二分法缩小范围）
condition函数具有单调性：如果某个值x满足condition(x)，那么所有大于等于x的值也必然满足condition(x)（比如“大于等于6”“是某个数的倍数”这类单调条件）
循环不变式定义
在每次循环开始前，以下三个条件始终成立：
right要么是满足condition的元素，要么处于搜索空间的右边界left要么是不满足condition的元素，要么处于搜索空间的左边界- 我们要找的第一个满足条件的元素，一定落在区间
[left, right]内
初始状态验证
初始时left = min(search_space)，right = max(search_space)：
- 整个搜索空间就是
[left, right]，目标元素必然在其中，满足第三个条件 - 此时
right和left的状态符合前两个条件，所以初始状态下不变式成立
循环过程中的不变式保持
每次循环计算mid = left + (right - left) // 2（这是避免整数溢出的写法，和(left + right) // 2结果一致，但不会因为大数相加溢出）：
- 如果
condition(mid)为真：说明mid是满足条件的元素，那更小的满足条件的元素可能在[left, mid]区间里，所以把right设为mid。此时新的right仍然满足condition，目标元素也还在[left, right]里，不变式保持。 - 如果
condition(mid)为假：说明mid不满足条件，根据单调性，所有小于等于mid的元素都不满足条件，所以目标元素只能在[mid+1, right]里，把left设为mid + 1。此时新的left要么不满足条件，要么就是目标元素，不变式保持。
循环终止条件
当left == right时，循环结束：
- 此时区间
[left, right]只有一个元素，根据不变式，这个元素就是我们要找的第一个满足条件的元素：- 如果
condition(left)为真，那它就是第一个满足条件的元素（因为之前的left都不满足，直到最后一步跳到这里） - 如果整个搜索空间都不满足条件，那
left等于right且condition(left)为假，此时可以根据问题需求返回对应结果（模板默认场景是存在有效元素）
- 如果
实例验证
比如在有序数组[1,3,5,7,9]中找第一个大于等于6的元素：
- 初始
left=1，right=9 - 第一次循环：
mid=(1+9)//2=5，condition(5)（>=6？）为假，所以left=5+1=6 - 第二次循环：
left=6 < right=9，mid=(6+9)//2=7，condition(7)为真，right=7 - 第三次循环：
left=6 < right=7，mid=(6+7)//2=6，condition(6)为真，right=6 - 此时
left==right=6，返回6，完全符合预期
关键细节说明
mid = left + (right - left) // 2：避免left + right溢出，比如当left和right都是极大整数时，直接相加会超出语言的整数范围- 循环条件
left < right：确保循环结束时left和right必然重合，不需要额外判断两者的关系 - 模板适用场景：所有需要寻找下界的问题，比如找插入位置、第一个大于目标值的元素、第一个符合条件的元素等
内容的提问来源于stack exchange，提问作者Web Knowledge
相关产品推荐
相关产品推荐
