ACM通信
制定正确的程序(2)
这是关于一个看似naïve的问题的第二篇文章:我们如何编写二进制搜索程序?更准确地说，我们如何编写二进制搜索程序正确的?
如果你还没有读过第一篇文章，请先读一遍(你可以找到它在这里.)，因为如果不这样做的话，这句话真的没有多大意义。
我们在寻找一种元素x在排序数组中t。第一个候选程序尝试是:
——程序尝试1号。
从
I:= 1;J:= n——结果初始化为0。
直到我=我循环
m:= (i + j) // 2——整数除法
如果T [m]≤x然后我:= m其他的j: = m结束
结束
如果X = t [i]然后结果:=我结束
问题是:这是正确的吗?如果是这样，它应该会产生正确的答案。(如果是其中之一，答案是正确的结果索引是否在t元素的x,或结果= 0而且x不会出现在t。)
这个程序不正确。要证明它是不正确的，只需一个程序不适合的例子(测试用例)就足够了。给出正确答案”。假设x = 1和数组t有两个元素都等于0 (n= 2，记住数组是从1开始索引的:
T = [0 0]
变量和表达式的连续值为:
M I j I + j + 1
在初始化:1 2 3
我≠j，因此输入loop:1 1 26——从t[1]开始的第一个if分支≤x
我得到了m的值
的值都没有我而且j已更改，因此循环将永远重复其主体(取第一个分支)。它甚至不是程序产生一个错误的答案:它根本没有产生一个答案!
请注意(参考第一篇文章中提到的著名的Dijkstra引用)，虽然将测试与证明相比较是很常见的，测试实际上可以是一种证明:失败的测试证明程序是不正确的。和最复杂的数学证明一样有效。它可能不是我们最喜欢的那种证明(我们的客户倾向于保证程序是正确的)，但它是一种不错的证明。
现在我们准备进行第二次尝试:
——程序尝试2号。
从
I:= 1;j: = n
直到我=我或结果> 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)，沙夫豪森理工学院(瑞士)教授和教务长，俄诺波利斯大学(俄罗斯)软件工程实验室负责人。
没有发现记录