每个程序员都应该会点形式化证明
我认为每个程序员都应该会点形式化证明，这有助于思考，更有助于写出正确的实现。
在最近的面试中，我发现近一半的面试者不能正确完成二分搜索（的一个变种）。这些面试者有些是有 3-5 年工作经验，有些是刚毕业的计算机专业的优秀学生。我很惊讶于他们没有一个人能够给出一个完整的，细致而全面的二分搜索算法的解释和正确实现。有些面试者尽管能够写出正确的算法，但是在后面的询问过程中发现他们并没有考虑清楚边界情况，只是恰好写对了。这不禁让我感叹，每个程序员都应该会点数学归纳法。
问题描述如下：给定一个单调非下降的数组，要求在其中进行二分搜索，找到第一个大于等于给定数字的位置（std::lower_bound）。这一限定是比较宽泛的，比如说没有限制每次递归中比较的次数，没有限定只能使用小于等于运算符，没有考虑没找到的情况下（目标位置溢出右边界）返回什么，等等。
为了更进一步的叙述方便，我在此说明一些记号的含义：
-
给定的目标元素记为
t。 -
给定的数组记为
arr，其长度为n。 -
arr[k]为数组中位置为k的值。 -
数组的连续子区间 \([b, e)\) 中含有
arr[b]，arr[b + 1]，…，arr[e - 1]的值。其中间元素的位置 \(m = b + \lfloor (e - b) / 2 \rfloor\)。
二分搜索的方法是，检查目标区间的中间元素与目标元素的大小关系，以此为依据将目标区间划分为 2 部分，然后在其中的一部分中继续进行上述步骤，直到目标区间足够小，能够简单的确定要查找的元素的位置。然后使用这一简单方法，确定最终要找的元素的位置。
一般来说，面试者会考虑三种情况：
-
arr[m]<t，此时需要在右侧区间（不含中间元素）\([m + 1, e)\) 中继续进行搜索。 -
arr[m]=t，此时需要在左侧区间（含中间元素）\([b, m + 1)\) 中继续进行搜索。 -
arr[m]>t，此时需要在左侧区间（含中间元素）\([b, m + 1)\) 中继续进行搜索。含中间元素的原因是有可能在给定的数组中没有和目标元素相等的元素。
这三种情况考虑的如果没有漏洞的话，就能保证*要找的元素始终在新的区间中*，记此性质为 Safety Property 1。
这一步是大多数面试者都能正确做到的。但是我见过的所有的面试者都没有去考虑这样一件事：新的区间是否比原区间小？事实上，我们需要保证*新的查找区间总是比原查找区间小*，这样算法才能够不断有进展，记此性质为 Liveness Property 1。
令 \(e = m + 1\)，解得 \(e = b + 1\) 或 \(e = b + 2\)，即查找区间有 1 个元素或 2 个元素。显然，\(b = m + 1\) 永远都不会成立。由此才能确定，当查找区间收缩到空区间或只含有小于等于 2 个元素时，需要进行特殊处理。所谓特殊处理，即是指处理违反 Liveness Property 1 的情况。此时一一检查区间中的元素即可，如果要找的元素不存在，此时返回 -1 或 e 都是合理的选择。这样的操作保证了*当查找区间中只有 1 个或 2 个元素时，能够返回要找的元素的位置*，记此性质为 Safety Property 2。这一性质对应数学归纳法中的起始步骤。
无需进行形式化证明，只需按照证明的思路进行思考，写出的程序就可以很有信心。