1. 尽管我们的二分搜索证明历经曲折，但是按照某些标准来衡量还是不够完善。你会如何证明改程序没有运行时错误（例如除数为 0、数值溢出、变量值超出声明的范围或者数组下标越界）呢？如果有离散数学的基础知识，你能否使用逻辑系统形式化来证明？
为了证明程序不会出现溢出错误，我们在不变式中添加条件 0 <= l <= n 和 -1 <= u <=n，这样我们就可以限定 l+u 的范围了。这两个条件还可以用于证明不会访问数组边界之外的元素。如果像书中 9.3 节一样定义假想的边界元素 x[-1] 和 x[n]，那么我们就能将 mustbe(l,u)形式化地定义为 x[l-1] 和 x[u+1]>t。
2. 如果原始的二分搜索对你来说太过容易了，那么请试试这个演化后的版本：把 t 在数组 x 中第一次出现的位置返回给 p（如果存在多个 t 的话，原始的算法会任意返回其中的一个）。要求代码对数组元素进行对数次比较（该任务可以在 log2n 次比较之内完成）。
l = -1; u = n
while l+1 != um = (l + u) / 2if x[m] < tl = melseu = m
p = u
if p >= n || x[p] != tp = -1
如果 t 在 x 中，那么将 p 置为 t 第一次出现的下标；如果 t 不在数组中，则将 p 置为 -1。
3. 编写并验证一个递归的二分搜索程序。代码和证明中的哪些部分与迭代版本的二分搜索程序相同？哪些部分发生了改变？
4. 给你的二分搜索程序添加虚拟的“计时变量”来计算程序执行的比较次数，并使用程序验证技术来证明其运行时间确实是对数的。
5. 证明下面的程序在输入 x 为正整数时能够终止。
while x != 1 doif even(x)x = x / 2elsex = 3 * x + 1
如果你解决了这个问题，请到最靠近的数学系申请一个博士学位。
6. [C.Scholten] David Gries 在其 Science of Programming 中将下面的问题称为“咖啡罐问题”。给定一个盛有一些黑色豆子和一些白色豆子的咖啡馆以及一大堆“额外”的黑色豆子，重复下面的过程，直至罐中仅剩一颗豆子为止：从罐中随机选取两颗豆子，如果颜色相同，就将它们都扔掉并且放入一个额外的黑色豆子；如果颜色不同，就将白色的豆子放回罐中，而将黑色的豆子扔掉。需要证明该过程会终止。最后留在罐中的豆子颜色与最初罐中白色豆子和黑色豆子的数量有何函数关系？
由于每一步都使得罐中的豆子减少一粒，所以该过程能够终止。我们每一步都从咖啡罐中拿掉零个或者两个白色豆子，所以白色豆子的奇偶性保持不变。因此，当且仅当罐中最初的白色豆子个数为奇数时，最后留下的豆子才可能是白色的。
7. 一位同事在编写一个在位图显示器中画线的程序时遇到了下面的问题。n 对实数（ai，bi）构成的数组定义了 n 条直线 yi = ai + bi。当 x 位于[0,1]内时，对于区间[0,n-2]内的所有 i，这些线段按 yi < yi+1 排序。用更形象的话说，这些线段在垂直方向上不交叉。给定一个满足 0 <= x <= 1 的点（x,y），他需要确定包围这个点的两条线段。他该如何快速解决该问题呢？
构成梯级的线段在 y 方向上是递增的，因此我们可以通过二分搜索来找到包含给定点的两条线段。搜索中的基本比较说明了点在给定线段的下方、里面还是上方。应如何编写该函数？
8. 二分搜索一般比顺序搜索要快：在含有 n 个元素的表中查找，二分搜索需要大约 log2n 次比较，而顺序搜索需要大约 n/2 次比较。通常情况下这已经足够快了，但是有些情况下，二分搜索必须执行得更快。虽然我们无法减少由算法决定的对数级的比较次数，你可以重新编写代码使之执行得更快吗？为明确起见，假定你需要搜索一个包含 1 000 个整数的有序表。
i = 512
l = -1
if x[511] < tl = 1000 - 512
while i != 1i = i / 2if x[l+i] < tl = l + i
p = l + i
if p > 1000 || x[p] != tp = -1
程序代码将确保 i 总是 2 的幂。该性质很容易保持，但是一开始难以获得（因为数组的大小 n 等于 1 000）。因此在程序的开始部分先使用了赋值语句和 if 语句，以确保初始的搜索范围大小为 512，即小于 1 000 的数中最大的 2 的幂。这样 l 和 l+1 一起要么表示 -1…511，要么表示488…1 000。使用这个新的范围表示方法转换初始的二分搜索程序。
因为 i 在程序中只有 10 个互不相同的值，所以我们可以将它们全部写在代码中，从而避免在运行时重复计算。代码如下：
l = -1
if (x[511] < t) l = 1000 - 512
if (x[l+256] < t) l += 256
if (x[l+128] < t) l += 128
if (x[l+64] < t) l += 64
if (x[l+32] < t) l += 32
if (x[l+16] < t) l += 16
if (x[l+8] < t) l += 8
if (x[l+4] < t) l += 4
if (x[l+2] < t) l += 2
if (x[l+1] < t) l += 1
p = l + 1
if p > 1000 || x[p] != tp = -1
9. 完成以下程序验证练习，准确说明以下每个程序片段的输入、输出动作，并证明代码可以完成其任务。第一个程序实现向量加法 a = b + c。
i = 0
while i < na[i] = b[i] + c[i]i = i + 1
(该代码和下面的两个代码片段使用末尾带有自增运算的 while 循环展开了 “for i = [0,n)”循环)。下面的代码片段计算数组 x 中的最大值。
max = x[0]
i = 1
while i < n doif x[i] > maxmax = x[i]i = i + 1
下面的顺序搜索程序返回 t 在数组 x[0…n-1]中第一次出现的位置。
i = 0
while i < n && x[i] != ti = i + 1
if i >= np = -1
elsep = i
下面的程序以正比于 n 的对数的时间计算 x 的 n 次方。该递归程序的编码和验证很简单；其迭代版本比较复杂，留作附加题。
function exp(x, n)pre n >= 0post result = x ^ n
if n = 0return 1
else if even(n)return square(exp(x, n/2))
elsereturn x * exp(x, n-1)
10. 在二分搜索函数中引入错误，观察验证错误代码时这些引入的错误是否会（以及如何）被捕获？
11. 使用 C 或 C++ 编写递归的二分搜索函数并证明其正确性，要求函数的声明如下：int binarysearch(DataType x[], int n)单独使用该函数，不要调用其他任何递归函数。
参考答案 11.14中把数组指针传递给 swap 函数的递归函数。
