How does Contract.Ensures work?

Question

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 ?

Answer 1

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.

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.

---

EDIT: 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.