ACM通信

BLOG@CACM

精神上的自我检查

Bertrand Meyer的
2022年1月19日
评论(2)

有些在精神病院的人认为外面的人是疯子;世界其他地区不同意这种说法。

如果你只是在里面或外面，这是很难裁决的问题。

用Eiffel和契约式设计编程是少数人的特权，他们认为世界上的其他人都疯了。例如，我根本不知道如何用其他方式编程并保持一个人的理智;但也许我才是疯子这篇文章可以作为精神上的自我检查。

简而言之:使用强大的静态类型系统和契合式设计从根本上改变了软件开发的本质，它变成了一种更可预测和愉快的努力，值得被称为“软件工程”。

让我从我正在编写的程序中举一个例子。我有几个数据结构，相当复杂。他们代表着油印，它类似于一个有向图，但有标记的边，并且在两个给定节点之间可能有任意数量的边(不只是0或1)，具有不同的标签。下图显示了多重图;节点表示人与房子，边表示人与房子之间的关系，例如一个人是另一个人的老板，房子是一个人的住所。

一个多重图

假设我们有一种方法用一个唯一的整数表示每个节点;上面示例的简化视图如下所示，显示节点编号(26和57，任意示例)和标记(spouse缩写为年代)仅为一条边:

多重图(局部视图)

表示这一概念的数据结构是“三重表”:一个三元组数组，每个三元组包含一个节点标识符x,一个标签t，和另一个节点y．典型的三表是这样的:

看看高亮显示的三倍triple_table表示多重图的图形说明中突出显示的边。三元表声明如下:

triple_table: HASH_SET(三)

在哪里HASH_SET(变种HASH_TABLE)是一个库类三倍一个类(不是来自库，而是为这个应用程序编写的)，描述有三个组件的对象:源，标签而且目标．一个HASH_SET是集合的一种实现，其中每个元素(这里是每个三元组)都充当自己的键。

这些类型声明已经为我们提供了很多帮助。例如，要找出表中是否存在具有特定值的三元组，您将使用测试

triple_table。有(创建{三}。Make (a_source, a_tag, a_target)

这里的所有内容都需要具有特定的类型。第一次编译尝试将许多错误作为类型错误扼杀在萌芽状态。

为什么有人会使用动态类型语言(用于10行脚本之外的任何东西)，而不使用这种神奇的bug消除机制，我不理解。但我得记住我是在精神病院。

事实证明，我的程序需要以多种不同的方式访问该结构。设计高效算法的一种常见技术是通过提供相同信息的几种(可能是冗余的)表示来交换一些空间以换取时间。这里有另一个数据结构很方便，triples_from,这样triples_from[我]条目列表在吗triple_table表示从我．这是triples_from [26]的例子:

获取具有给定源的三元组列表

triples_from [26]如图所示，为我们提供了第一个元素(源)为26的条目列表。

类型的情况现在变得更加令人兴奋:新结构的声明是

triples_from: ARRAY [LIST]
——从给定对象开始的三元组。按对象编号索引。

triples_from是一个三元组列表的数组。我们可以用它做很多事情，比如对整个结构进行迭代，并在每一步对相应的列表进行迭代。而且，我们会比以前搞得更糟!数据结构越复杂，错误的来源就越多;如果错误地将list当作list元素来使用，该怎么办?如果没有静态类型，这些常见的错误将不得不在测试期间被检测和修复，从而保证几个愉快的调试之夜。但是静态类型再次帮助我们。当我访问表中最后一个三元组的元素时，我必须这样写

.last.tag (triples_from[我])

任何混淆会立即被标记为类型不匹配:一个整数，其中列表是预期的，当它是列表时，使用一个结构体作为数组……

对于无类型语言，运行时结构看起来并不比意大利面盘好多少(只是没那么开胃)。

一旦出了什么问题，你就只能一根一根地拉扯，试图理解到底发生了什么。静态类型为数据提供结构，并在编译时捕获许多错误，这些错误可能需要数小时或数天的复杂调试。

对于我的多重图，我需要更多的访问模式。其实，我需要的不仅仅是高效存取源的三倍年代,还来自另外两个组成部分，标签和目标。确实有一张桌子triples_to，我没有在这里说明，因为它类似于triples_from；而且triples_with，它给出了带有给定标签的三元组列表:

带有给定标签的三元组(带有给定标签的多重图边)

即使这样也不是最后的结论。我还需要快速访问给定节点的“后继器”。下面是该结构的声明:

HASH_TABLE表列表，INTEGER类型

现在我们讨论的是正事:一个由三元组列表组成的哈希表数组，每个列表与一个整数相关联。

在这一点上，使用未输入的语言(以收容所囚犯的谦虚观点)等同于职业过失。对该结构的典型访问(设置三重组件中的一个的值)如下

triple_successors[我]。我tem (j).i_th (k).set_target (l)

很多事情都可能出错，你需要帮助。只有当一个强大的类型系统(具有继承、泛型等)支持它并且相关的编译器消除它时，您才能确信您得到的是您想要的。如果没有这样的类型系统，编程看起来就不像工程，而更像一连串的《万福玛利亚》。

类型检查是必要的，但它们只是第一步。仍然有许多原因会造成数据结构的不一致。在我的示例中，上面描述的几个互补的数据结构是同一信息的不同方面(或者，对于其中每个数据结构，是该信息的一部分)。他们必须是兼容的!

相应的类有几十个契约式设计条款来指定它们的角色:陈述个别操作属性的前提条件和后置条件，以及一个广泛的类不变式——截至今天，超过20个条款——说明各种结构如何彼此关联。这里有一个从句，一个“适用于所有人”的三级属性:

successors_consistent:

∀t: triple_继承者μ - t:三元组列表的哈希表，由(整数)标签索引
∀l: t μ - l:三元组列表
——(@l。关键我年代a key in the hash table:
——一个表示标签的整数。)
∀p: l μ——p:三倍
p.tag = @t。关键而且p.source = @t.cursor_index

(这些评论不是针对本文的，而是取自原文，作为良好文档实践的一部分，以帮助读者理解发生了什么。另外，请注意这是实际的类文本;艾菲尔使用Unicode符号，例如∀而且∃， EiffelStudio IDE将为您生成，不过如果愿意，您也可以使用关键字语法。)

这个例子依赖于这样一个特性:埃菲尔的量化比通常的量化(with∀或∃)谓词演算。在数学中，能写出这样的东西就足够了

∀x: L μ some_property (x)

表示列表或其他结构的所有元素l满足给定的性质。在编程中，可能还需要访问连续的元素x比如它在列表中的位置，或者ifl是哈希表，键与元素相关联吗x．埃菲尔符号@x，表示抽象游标，从中我们可以获得位置和键(分别为@x.cursor_index而且@x.key)．例如,如果l列表[1,4,9,16,25]满足这个性质吗

∀x: L μ x = (x.cursor_index) ^ 2

声明每个元素都是其在列表中的下标的平方。

上面显示的3级深度不变子句，为了方便起见，我在这里重复一下(没有注释)

∀t: triple_继承者μ∀l: t μ∀p: l μ p.tag = @t。Key和p.source = @t.cursor_index

简单地表达如下。考虑每一个元素triple_successors，这是一个哈希表(我们总是从类型声明中看到确切的类型);然后考虑哈希表中的每个元素，它是一个三元组列表(记录在哈希表中的整数键下)@l.key；最后考虑列表中的每一个三元组。那么这个三元组的三个分量(源，关键而且标签)满足所示的一致性属性，将它们连接到哈希表元素的键以及哈希表在整个哈希表列表中的位置。

以我的经验，如果没有对其属性的这种语义说明，编写这样的非平凡软件(尤其是具有复杂数据结构的软件)是完全不可能的。

顺便说一下，编写这些合同设计属性并不难;当然，这比在出现错误时调试代码要容易得多。(调试，也就是说试图根据一个程序失败的执行找出它的错误，这是世界上存在的最困难的智力挑战。更荒谬的是，有些人声称契约式设计很难。契约式设计很容易学习和应用。调试需要大量的脑力劳动。)

编写这样的不变属性不仅仅是记录您正在做什么，或者您认为您正在做什么。它也是一个工具检查，在强大软件工具的帮助下，你真的在做!在开发Eiffel程序和运行示例案例时，我打开了EiffelStudio提供的契约监视。这种机制会检查每一个合同条款，在每一次执行中(在开发过程中，而不是在操作过程中，一旦一切都被验证)。在我当前程序的实际运行中，这个属性意味着数百万个单独的支票。

每当软件的任何部分修改结构的任何部分时，该机制就会评估我在整个开发过程中耐心积累的每一个一致性属性。(当然不是在结尾，而是贯穿始终。像2022年疯人院内外的所有人一样，我实践了敏捷风格:在代码中添加一点——在我的例子中是所有契约元素——设计一个新测试，立即运行所有现有测试和新测试，直到所有测试都运行正常才继续。)

任何错误，无论多么具体或边缘，都有很大的机会被这些单独的检查发现。相反，一旦回归测试套件运行了数以百万计的独立一致性检查而没有违反，那么仍然存在重大错误的可能性就很低。传统开发中的“成功测试运行”与此环境中的“成功测试运行”有很大的区别，前者什么都不告诉您(通过了一个案例——那又怎样?)，而后者不仅告诉我们预期的结果，而且还告诉我们整个计算验证了每一个被认为是相关的一致性约束。

这种开发模式如此明显，如此明显地是“软件工程”中仅仅使用“工程”这个词的结果，以至于我不知道为什么仍然有人不做它。这种方法显然需要埃菲尔铁塔(几十年来在语言和环境中模拟契约式设计的数百次尝试都失败了)，因为这些想法必须在所有级别上得到支持:

• 该方法从需求开始应用契约式设计技术(以及完整的类型系统、继承和其他基本机制)，并贯穿整个设计和实现。
• 该语言完全支持契约机制。特别要注意的是，虽然您可以在没有配备契约式设计结构的语言中在一定程度上模拟前置条件和后置条件，但这样的解决方案不适用于类不变量，因为类不变量必须是语言的一部分。如上例所示，类不变量是该方法的关键元素。此外，前置条件和后置条件在继承上下文中具有特殊的语义(分别是弱化和加强，以允许安全的多态性和动态绑定)，这需要语言和编译器的支持。例外情况也与合同密切相关。
• 环境EiffelStudio提供了在运行时启用和禁用契约监视的机制。通常，您可以在开发过程中启用所有检查，就像我现在所做的那样，然后一旦确信代码的正确性，就可以关闭它进行部署和操作。(作为一种软件容错机制，有些检查可能会继续，但这是另一个讨论的内容。)

当我被剥夺了这些机制时，我觉得生产软件就像1960年那样:最终是可能的，但以偶然的努力为代价。你写了一些代码，然后你发现它不太工作。然后，在剩下的过程中，你会用各种各样的调试见解和福尔摩斯式的推理技巧，在不可预测的时间内找出可能的错误。然后你试图解决这个问题，然后继续下一个问题。我们怎么能用“软件工程”这样的词来恭维自己这样的过程呢?对我来说，工程学意味着用我们正在做的知识去做一些事情。(我知道“软件工程”应该是什么意思，我在重复我自己的话。但这对孩子和疯子是可以容忍的。)

知道我们在软件中做什么，意味着要写出与各种元素相关联的精确语义属性。

你仍然会在这个过程中搞砸，因为我们都是这样，但过程是完全不同的。当你找到原因，而不仅仅是症状时，它就变得可以预测了。错误是代码应该做什么和它能做什么之间的差异。除非我们明确指出我们所期望的行为的要点，否则我们怎么能认真地铲除漏洞并使我们的软件正确呢?

一旦您转向这种将软件开发视为实际工程的理性形式，视角的变化将是惊人的。这就好像是一门不同的学科。但当然，这种经历来自精神病院的人，可能完全是幻觉。请告诉我，我是那个疯子吗?

Bertrand Meyer他是瑞士沙夫豪森理工学院的教授和教务长，Innopolis大学的客座教授，埃菲尔软件公司的首席技术官。

---

评论

---

显示所有2评论