ACM通信
制定正确的计划(2)
这是关于一个看似naïve问题的第二篇文章:我们如何编写二进制搜索程序?更准确地说，我们如何编写二进制搜索程序正确的?
如果你还没有读过第一篇文章，请先读一下(你可以找到它在这里.)，否则这句话真的没有多大意义。
我们在找一个元素x在一个排序数组中t．第一个候选程序的尝试是:
程序尝试#1。
从
I:= 1;J:= n——结果初始化为0。
直到I = j循环
m:= (i + j) // 2——整数除法
如果T [m]≤x然后I:= m其他的J:= m结束
结束
如果X = t [i]然后结果:= i结束
问题是:这是正确的吗?如果是这样，它应该会得到正确的答案。(答案是正确的结果索引是t一个元素等于x,或结果= 0而且x没有出现在t．)
这个程序不正确。要证明它不是正确的，只要有一个程序不正确的例子(测试用例)就足够了。给出正确答案”。假设X = 1还有数组t有两个元素都等于零(n= 2，记住数组是从1开始索引的:
T = [0 0]
变量和表达式的连续值为:
M I j I + j + 1
在初始化:1 2 3
I≠j，因此输入循环:1 1 26——t[1]以来if的第一个分支≤x
我得到了m的值
的值都没有我而且j已经改变，因此循环将永远重复其主体(取第一个分支)。这甚至不是程序产生了一个错误的答案:它根本没有产生一个答案!
请注意(参考第一篇文章中提到的著名的Dijkstra引用)，虽然将测试与证明对立起来是很常见的，测试实际上可以是证明:失败的测试证明程序是不正确的。和最复杂的数学证明一样有效。这可能不是我们最喜欢的那种证明(我们的客户往往更喜欢保证程序是正确的)，但这是一种很好的证明。
我们现在准备进行第二次尝试:
程序尝试#2。
从
I:= 1;J:= n
直到I = j或结果> 0循环
m:= (i + j) // 2——整数除法
如果T [m]≤x然后
I:= m + 1
elseifT [m] = x然后
结果m: =
其他的——在本例中，t [m] > x
J:= m - 1
结束
结束
与前一个版本不同，这个版本总是在变化我或j，所以我们可能希望它不会永远循环。它之间有很好的对称性我而且j．
和之前一样的问题:这个项目达到它的目标了吗?
周一回答。
出版报告:已公布的第三篇(“星期一”)文章已发表在这里．
Bertrand Meyer首席技术官是埃菲尔铁塔的软件(Goleta, CA)，沙夫豪森理工学院(瑞士)的教授和教务长，以及Innopolis大学(俄罗斯)软件工程实验室的负责人。
没有找到条目