代码合同：我们是否必须在委派方法中冗余地指定 Contract.Requires(...) 语句？

Question

我打算在未来的开发中使用新的 .NET 4 代码合同 功能。这让我想知道我们是否必须在方法链中冗余地指定等效的 Contract.Requires(...) 语句。

我认为一个代码示例值一千字：

    public bool CrushGodzilla(string weapon, int velocity)
    {
        Contract.Requires(weapon != null);

        // long code

        return false;
    }

    public bool CrushGodzilla(string weapon)
    {
        Contract.Requires(weapon != null);   // specify contract requirement here
                                             // as well???

        return this.CrushGodzilla(weapon, int.MaxValue);
    }

对于运行时检查这并不重要，因为我们最终总会遇到需求检查，如果它失败了我们会得到一个错误。

但是，当我们在第二次重载中没有在此处再次指定合同要求时，是否被认为是不好的做法？

另外，还会有编译时检查的功能，可能还有代码合约的设计时检查。似乎它在 Visual Studio 2010 中还不能用于 C#，但我认为像 Spec# 这样的一些语言已经可以使用。当我们编写代码来调用这样的方法时，这些引擎可能会给我们提示，而我们的参数目前可以或将是null。

所以我想知道这些引擎是否会一直分析调用堆栈，直到找到当前不满足合约的方法？

此外，here I learned about the difference between Contract.Requires(...) and Contract.Assume(...)。我想这个区别也应该在这个问题的背景下考虑？

Answer 1

我认为最好在每个公共方法上指定所有合同。合同不仅仅是“检查的内容”——它也是有效的文档。如果您调用了一个方法但不知道应用了哪个合约，那么将合约失败降到更低会很奇怪：这表明您正在调用的方法中存在错误，而不是 您的 em> 方法。

请注意，如果您在整个项目中使用 C# 4，则可以考虑使用可选参数和命名参数来避免过多的重载。当然，如果您需要从不支持它们的语言调用代码，这将没有用处。

我强烈怀疑如果你没有在“默认”重载中指定合约，静态检查器（是现在available for all versions of VS2010）会抱怨合约可能会失败，并且会还建议添加合同。

Answer 2

另外，还会有 编译时检查，并且可能 代码的设计时检查 合同。在 Visual Studio 2010 中似乎还不能用于 C#...

它可用，但要使其工作，您必须使用 VS2010 Ultimate 版本。

警告：这有点推测，但从我使用它所学到的知识来看似乎是正确的；

您需要通过您的方法手动传播约束，就像您所做的那样。

代码契约可以从方法外部看到的唯一信息就是你告诉它的信息。它可以检查方法内部的假设和断言，但这种分析不会传播。换句话说，CC 无法“看穿”您的方法，因此它不会自动知道 CrushGodzilla(string) 将要求 weapon 为非空。

如果使用静态分析，它会在CrushGodzilla(string) 中进行检查并意识到weapon 不能为空，使用关于CrushGodzilla(string,int) 的external 信息，它会建议您添加一个Requires 非空前提条件。 （不传播是指这些知识不会用于分析程序的其余部分。）

尽管看过，我实际上还没有找到任何地方很好地记录了该静态分析器。