Contract.Ensures 是如何工作的？答案

【问题标题】：How does Contract.Ensures work?Contract.Ensures 是如何工作的？
【发布时间】：2011-08-13 19:00:53
【问题描述】：

我开始使用代码合同，虽然 Contract.Requires 非常简单，但我无法看到 Ensures 的实际作用。

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

static void Main()
{
    DoSomething();
}

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

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

那么它实际上是做什么的呢？

【问题讨论】：

我开始你的例子，并在向控制台写入了一些东西后得到了一个未处理的异常ContractException“后置条件失败：错误错误”。所以看起来效果不错。
静态证明者是代码合约背后的真正价值，尽管从分析上讲，这确保条件非常奇怪。大致相当于要求一个人证明“这句话是假的”的真实性。
虚假部分只是为了确保它被触发:-)
@Dan Bryant：实际上，它是有用的。你可以用它来标记永远不会返回的方法，所以如果你有一些调用（例如）Environment.Exit，你可以用Contract.Ensures(false)标记它。然后静态检查器可以使用此信息。

标签： c# code-contracts

【解决方案1】：

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

Contract.Ensures 令人困惑的地方在于，您在方法的开头编写它，但它在方法的结尾执行。重写器会尽一切努力确保它正确执行，并在必要时获得返回值。

就像许多关于代码契约的事情一样，我认为最好在重写器工具的结果上运行 Reflector。确保你的设置正确，然后弄清楚重写器做了什么。

编辑：我意识到我还没有表达Contact.Ensures 的观点。简而言之，它是为了确保您的方法在最后完成了某些操作 - 例如，它可以确保将某些内容添加到列表中，或者（更有可能）返回值是非 null、正数或其他值。例如，您可能有：

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;
}

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

【讨论】：

你是对的 - 项目设置中的模式设置错误。我的愚蠢错误:-)
@Steffen：我添加了更多内容以使其更清楚它的含义。我不知道您是否需要它，但未来的读者可能会发现它很有用:)
很好的阐述 - 这几乎是我所期望的，但写下来总是很好:-)
在您给出的示例中，output 的值将与input 的 current 值进行比较，对吗？所以如果你想将它与参数的初始值进行比较，你需要Contract.Ensures(Contract.Result<int>() > Contract.OldValue<int>(input))?
@JustinMorgan：听起来不错——当然只有在代码中更改参数值才重要，我很少这样做。