c# - Contract.Ensures 是如何工作的？

Question

我开始使用 Code Contracts，虽然 Contract.Requires 非常简单，但我很难理解 Ensures 的实际作用。

我试过创建一个像这样的简单方法:

static void Main()
{
    DoSomething();
}

private static void DoSomething() 
{
    Contract.Ensures(false, "wrong");
    Console.WriteLine("Something");
}

虽然我从来没有看到“错误”的消息，也没有抛出异常或其他任何东西。

那么它到底做了什么？

Answer 1

它不抛出任何东西很奇怪 - 如果您正在使用适当的设置运行重写器工具。我的猜测是您正在以不检查后置条件的模式运行。

关于 Contract.Ensures 的令人困惑的事情是你写它在方法的开始，但它执行在方法的末尾方法。重写器会施展所有魔法以确保其正确执行，并在必要时获得返回值。

与代码契约的许多事情一样，我认为最好在重写工具的结果 上运行 Reflector。确保您的设置正确，然后找出重写器做了什么。

---

编辑:我意识到我还没有表达Contact.Ensures 的点。简而言之，它是为了确保您的方法在最后完成了一些事情——例如，它可以确保它向列表中添加了一些东西，或者(更有可能)返回值是非空的、正的或其他什么。例如，您可能有:

public int IncrementByRandomAmount(int input)
{
    // We can't do anything if we're given int.MaxValue
    Contract.Requires(input < int.MaxValue);
    Contract.Ensures(Contract.Result<int>() > input);

    // Do stuff here to compute output
    return output;
}

在重写的代码中，返回点将进行检查，以确保返回值确实大于输入。