如何Contract.Ensures工作？ [英] How does Contract.Ensures work?

问题描述

我开始使用代码契约，并同时Contract.Requires是相当直接的，我无法看到的究竟是什么呢确保

I'm starting to use Code Contracts, and whilst Contract.Requires is pretty straight forward, I'm having trouble seeing what Ensures actually does.

我已经尝试创建这样一个简单的方法：

I've tried creating a simple method like this:

static void Main()
{
    DoSomething();
}

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

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

I never see the message "wrong" though, nor does it throw exceptions or anything else.

那么，它实际上做什么？

So what does it actually do ?

推荐答案

它不扔东西很奇怪 - 的如果的你正在运行使用适当的设置重写工具。我的猜测是，你在不检查后置模式运行。

It's odd for it to not throw anything - if you're running the rewriter tool with the appropriate settings. My guess is that you're running in a mode which doesn't check postconditions.

有关的令人困惑的事情 Contract.Ensures 是写的它在方法的开始，但它的执行的在方法的末尾。重写做所有的魔法，以确保它执行正确，并且给出如果有必要的返回值。

The confusing thing about Contract.Ensures is that you write it at the start of the method, but it executes at the end of the method. The rewriter does all the magic to make sure it executes appropriately, and is given the return value if necessary.

就像关于代码契约很多事情，我认为这是最好的运行反射镜上重写工具的结果的。请确保你有正确的设置，然后制定出什​​么重写做

Like many things about Code Contracts, I think it's best to run Reflector on the results of the rewriter tool. Make sure you've got the settings right, then work out what the rewriter has done.

编辑：我知道我没有表示的点的 Contact.Ensures 还没有的。简单地说，这是确保你的方法已经被最终做了一些 - 例如，它可以确保它的补上一到列表，或者更有可能的返回值不为null，或正或什么的。例如，你可能有：

I realise I haven't expressed the point of Contact.Ensures yet. Simply put, it's to ensure that your method has done something by the end - for example, it could ensure that it's added something to a list, or (more likely) that the return value is non-null, or positive or whatever. For example, you might have:

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

在改写码，将有一个检查在点返回的，以确保返回的值真正的是的大于输入。

In the rewritten code, there will be a check at the point of return to ensure that the returned value really is greater than the input.

这篇关于如何Contract.Ensures工作？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！