由合同和施工方设计

Question

我正在出于学校目的实现我自己的 ArrayList，但为了让事情变得有趣一点，我尝试使用 C# 4.0 代码契约。一切都很好，直到我需要将合同添加到构造函数中。我应该在空参数构造函数中添加 Contract.Ensures() 吗？

    public ArrayList(int capacity) {
        Contract.Requires(capacity > 0);
        Contract.Ensures(Size == capacity);

        _array = new T[capacity];
    }

    public ArrayList() : this(32) {
        Contract.Ensures(Size == 32);
    }

我想说是的，每种方法都应该有一个明确定义的契约。另一方面，如果它只是将工作委托给“主”构造函数，为什么要放置它呢？从逻辑上讲，我不需要。

我认为在两个构造函数中显式定义合约有用的唯一一点是，如果将来我们对合约有 Intelisense 支持。如果发生这种情况，明确每个方法具有哪些契约会很有用，就像 Intelisense 中出现的那样。

另外，是否有任何书籍可以更深入地介绍契约设计的原理和用法？一件事是了解如何在一种语言（本例中为 C#）中使用合约的语法，另一件事是知道如何以及何时使用它。我阅读了一些教程和 Jon Skeet 的 C# in Depth 文章，但如果可能的话，我想更深入地了解一下。

谢谢

Answer 1

使用 ArrayList 的客户端代码（使用代码契约）不会知道空构造函数Ensure是Size == 32，除非您明确声明所以使用Ensure。

所以（例如）：

var x = new ArrayList();
Contract.Assert(x.Size == 32)

会给你警告“断言未证明”。

您需要明确说明所有合同；代码合约重写器/静态检查器不会“查看”方法来查看任何含义 - 请参阅 我对相关问题的回答“我们是否必须在委托方法中冗余地指定 Contract.Requires(…) 语句？”

Answer 2

我建议阅读面向对象的软件构建，第二版，或者Touch of Class，均来自 Bertrand Meyer。或者，您可以阅读 1992 年的文章 应用“Design by Contract” 来自同一作者。

总结一下：

• 类不变量必须在构造函数（其中任何一个）完成之后以及类的任何公共方法执行之前和之后保持不变。
• 方法前置条件和后置条件是进入和退出任何公共方法时必须保持的附加条件以及不变量。

因此，就您的情况而言，请关注不变量。无论调用哪个构造函数，都会生成一个正确的对象（满足类不变量的对象）。

在此 相关答案 我讨论了类似的主题，包括一个例子。

Answer 3

嗯，我不完全明白为什么你把“Ensures”也放在默认的c'tor中。因为它调用了主 c'tor，而主 c'tor 已经实现了完整的合约，所以默认的 c'tor 也会按照定义执行此操作。所以这是一个逻辑冗余，因此是一个很大的“不要”。也许它可能具有务实的含义，就像你说的 - 不知道代码契约那么好......

关于文献 - 最好的来源是：

• 按契约设计，按示例（书籍，Addison-Wesley）
• 关于该问题的维基百科文章
• 契约式设计简介（Eiffel 系列，但 DbC 原则不特定于语言）

HTH！
托马斯

Answer 4

按契约设计源自函数式编程的数学根源：先决条件 和 后置条件。

你真的不需要一本关于它的书，它最多只是计算机科学学位的一个章节（大多数会教授这个概念）。基本前提是您编写函数期望的前提条件以及给定正确参数时它将产生的输出。该函数预计不会在初始参数不正确的情况下运行。对于算法来说也是如此：它是绝对可靠的，即它保证提供预期的结果。

这就是我在目前正在学习的学位中所学到的，不过可能有更好的定义。维基百科关于契约设计的文章是带着面向对象的倾向编写的，但前置/后置条件是独立于语言的。

Answer 5

我完全不同意托马斯的回答。只要您在 ArrayList() 的实现中做出选择，您就应该签订一份合同来记录这些选择。

在这里，您选择使用参数 32 调用主构造函数。您可以决定做许多其他事情（不仅仅是关于默认大小的选择）。为 ArrayList() 提供一个与 ArrayList(int) 文档几乎相同的合同，您决定不做大多数您可以做的愚蠢的事情，而不是直接调用它。

答案“它调用主构造函数，因此让主构造函数的合约完成这项工作”完全忽略了这样一个事实：合约的存在是为了让您不必查看实现。对于基于运行时断言检查的验证策略，即使对于几乎直接调用另一个构造函数/方法的如此短的构造函数/方法，编写契约的缺点是您最终会检查两次。是的，这似乎是多余的，但运行时断言检查只是一种验证策略，DbC 的原理与其无关。原则是：如果可以调用，就需要一个合约来记录它做了什么。