Contract.Ensures如何工作？

Question

我开始使用代码合同，虽然Contract.Requires非常直观，但是我不太明白Ensures实际上是做什么的。

我尝试创建一个简单的方法：

static void Main()
{
    DoSomething();
}

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

我从未看到过“wrong”这个消息，它也不会抛出异常或其他任何东西。

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

- Steffen

---

我开始运行你的示例，然后在向控制台输出了一些内容后遇到了一个未处理的异常ContractException，错误信息是"后置条件失败：false 错误"。所以看起来它工作得很好。 - kyrylomyr

静态证明器是代码合同背后的真正价值，尽管这个确保条件在分析上相当奇怪。从分析角度来看，它大致相当于要求一个人证明“这个陈述是假的”的真实性。 - Dan Bryant

假的部分只是为了确保它被触发 :-) - Steffen

@Dan Bryant：实际上，它是有用的。您可以使用它来标记永远不会返回的方法，因此如果您有调用（例如）Environment.Exit的内容，您可以使用Contract.Ensures(false)进行标记。静态检查器随后可以使用此信息。 - porges

Answer 1

如果你使用适当的设置运行重写工具，那么不抛出任何内容是很奇怪的。我猜测你可能在运行不检查后置条件的模式下。

Contract.Ensures 让人感到困惑的地方在于你需要在方法开头编写它，但是它却在方法结束时执行。 重写程序会通过一些魔法确保它正确执行，如果必要还会给出返回值。

和 Code Contracts 的许多内容一样，我认为最好对重写工具结果运行 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;
}

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

- Jon Skeet

---

你是对的 - 项目设置中的模式设置错误了。这是我犯的愚蠢错误 :-) - Steffen

@Steffen：我添加了一些内容，以使其更清晰地表达其意图。我不知道你是否需要它，但可能将来的读者会发现它有用 :) - Jon Skeet

不错的阐述-这基本上是我预期的，但有文字记录总是很好的 :-) - Steffen

在你提供的例子中，output 的值将与 input 的当前值进行比较，是这样吗？因此，如果您想将其与参数的初始值进行比较，您需要使用 Contract.Ensures(Contract.Result<int>() > Contract.OldValue<int>(input)) 吗？ - Justin Morgan

@JustinMorgan：听起来没错 - 当然，只有在你很少改变代码中的参数值时才会有影响。 - Jon Skeet

好像是明智的做法。感谢解释。 - Justin Morgan