Contract.Ensures如何运作？

Question

我开始使用代码合同,虽然Contract.Requires非常简单,但我很难看到Ensures实际上做了什么.

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

static void Main()
{
    DoSomething();
}

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

我从来没有看到消息"错误",也没有抛出异常或其他任何东西.

那它实际上做了什么？

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

在重写代码,会出现一个检查在返回点,以确保返回的值确实是大于输入.