ACM通信
把程序做对(1)
一位教员同事最近邀请我在他的一门课上做一个关于公理化语义的简短概述。我已经教授软件验证课程很长一段时间了。在这里)，所以我有充足的素材;但我决定花一点时间来解释为什么有一个系统的软件验证方法是好的，而不是仅仅重用它。
如果对软件专业人员或少数精英部门以外的计算机科学学生说“软件验证”，他们中的大多数人会想到“测试”。例如，在工作面试中，向程序员展示一个基于循环的算法，并问“你如何验证它?”:大多数人将开始讨论如何设计聪明的测试用例。
远非我来痛斥测试[1];事实上，我一直认为Dijkstra关于测试的那句不可避免的名言——它只能显示错误的存在，而不能显示错误的不存在[2]——每个人似乎都认为这是对测试的控诉和否定(它的作者可能就是这么想的)实际上是一个很好的广告为测试:一种发现bug的方法?是的!太棒了!我在哪里买?但这与验证软件是不一样的，后者意味着试图确定它已经存在没有bug。
除非听众意识到验证不仅仅意味着测试，否则关于公理语义或其他证明技术的最好的课程材料将不会引起任何兴趣。事实上，在某个地方有一个伟大的测试和公开演讲大师James Whittaker的演讲视频，他告诉他的观众不要担心，这不是一个标准的无聊的演讲，他不会开始讲循环不变量[3]!(循环不变量将在本系列文章中出现，事实上，它们是它的中心概念之一，但不是今天，所以先不要带睡袋。)所以我决定先举个例子来开始我的讲座不使用适当的验证。事实上，不止一个例子，你会看到的。
关于这篇文章及其追随者的一个警告:这里没有什么新内容。我用的是我1990年的书中的一个例子编程语言理论导论(练习9.12)。再往前追溯，1983年的《编程珍珠》ACM通信Jon Bentley[4]的文章用同样的基本思想阐述了同样的例子。然而，近四十年过去了，这些理念在从业者中仍不广为人知。因此，可以将这些文章看作是另一篇关于软件工程基础知识的教程。
辅导课是一个小测验。我们从一个程序文本开始:
从
I:= 1;J:= n——结果初始化为0。
直到I = j循环
m:= (i + j) // 2——整数除法
如果T [m]≤x然后I:= m其他的J:= m结束
结束
如果X = t [i]然后结果:= i结束
所有变量都是整数类型。t是一个已排序的整数数组，索引从1到n．让我们不要让任何符号影响朋友之间的关系。一个循环从p直到e循环问结束执行p然后，重复:停止如果e(退出条件)为true，否则执行问．(如{p;虽然不是e做{你}}的其他符号。)”: =“是赋值”，=“相等测试”。//是整数除法，例如。6 //3 = 7 //3 = 2．结果是特殊变量的名称，该变量的最终值将由此计算返回(作为函数的一部分，但我们只查看函数体)。结果像所有整数变量一样自动初始化为零，所以如果执行不赋值给什么结果函数将返回零。
第一个问题:这个程序试图做什么?
好吧，这不是真正的测试。我假设你知道答案:这是一种尝试“二分搜索”的方法，它在数组中找到一个元素，或者在大约的序列中确定它是否存在日志2(n)步骤，而不是n如果我们使用顺序搜索。(记住，我们假设数组是排序的。)结果应该给我们一个位置在哪里x出现在数组中，否则为零。
现在是真正的测试:这个项目达到这个目标了吗?
答案不是“是”就是“不是”。(如果没有，我不是在要求一个正确的版本，至少现在还没有，无论如何你可以在文献中找到一些。)这种情况是非对称的，我们可以说波伯利式的
- 要证明一个否定的答案，就需要一个单例如，一个特定的数组t和一个特定的值x，该程序设置失败结果这是应该的。
- 为了证明一个肯定的答案，我们需要提供一个可信的论据每一个t而且x程序集结果这是应该的。
如果你愿意，你可以在评论区找到答案。我自己的答案将在两天后(星期三)揭晓。
出版报告宣布的第二篇文章发表了在这里．
笔记
[1]的TAP会议系列(Yuri Gurevich和我发起的《测试与证明》)探讨了两种方法之间的互补性。
Dijkstra于1969年首次发表了他的观察结果。他不需要考虑无限输入集的情况:即使是一个简单的有限程序，它乘以两个32位整数，要检查的情况的数量是264，是人类无法企及的。今天的64位整数更是如此。从2020年的角度来看这一点，我们可能会注意到，对有限情况集的彻底测试，Dijkstra认为在实践中不可能，实际上正是受尊重的模型检查验证技术可以;不是用原来的程序，而是用简化的抽象——精确设计的版本，以保持案件的数量可控。Dijkstra的论证仍然有效，当然，如果原始程序不是平凡的。而且模型检查并不能让我们走出困境:如果它的“测试”没有发现bug，我们是安全的，如果它发现了bug，我们必须确保bug是原始程序的属性，而不是抽象过程的产物。
它在YouTube上的某个地方，虽然我现在找不到。
[4]乔恩·本特利:编程珍珠:编写正确的程序,在ACM通信第26卷第4期。第12页，第1040-1045页，1983年12月，例如在这里．
Bertrand Meyer首席技术官是谁埃菲尔铁塔的软件(Goleta, CA)，沙夫豪森理工学院(瑞士)教授和教务长，俄诺波利斯大学(俄罗斯)软件工程实验室负责人。
没有找到条目