20

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 ?

Steffen
  • 13,648
  • 7
  • 57
  • 67
  • 1
    I started you example and got an unhandled exception `ContractException` "Postcondition failed: false wrong" after writing Something to the console. So looks like it works good. – kyrylomyr Aug 13 '11 at 19:08
  • The static prover is the real value behind code contracts, though this particular ensures conditions is quite odd, analytically speaking. It's roughly equivalent to asking a person to prove the truth of "this statement is false." – Dan Bryant Aug 13 '11 at 19:58
  • 2
    The false part was merely to ensure it was triggered :-) – Steffen Aug 13 '11 at 21:11
  • @Dan Bryant: Actually, it has a use. You can use that to mark methods that never return, so if you have something that calls (e.g.) `Environment.Exit`, you can mark it with `Contract.Ensures(false)`. The static checker can then use this information. – porges Aug 14 '11 at 03:43

1 Answers1

24

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.

Jon Skeet
  • 1,421,763
  • 867
  • 9,128
  • 9,194
  • You were right - the mode was set wrong in the project settings. Stupid mistake on my part :-) – Steffen Aug 13 '11 at 19:07
  • 2
    @Steffen: I've added a bit more to make it clearer what it's meant for. I don't know whether you needed that or not, but possibly future readers may find it useful :) – Jon Skeet Aug 13 '11 at 19:11
  • Nice elaboration - that was pretty much what I expected it to do, but it's always nice to have it in writing :-) – Steffen Aug 13 '11 at 19:39
  • In the example you've given, the value of `output` would be compared to the *current* value of `input`, is that right? So if you wanted to compare it to the parameter's initial value, you'd need `Contract.Ensures(Contract.Result() > Contract.OldValue(input))`? – Justin Morgan - On strike Dec 05 '12 at 22:05
  • @JustinMorgan: That sounds right - of course it only matters if you change the parameter value in the code, which I rarely do. – Jon Skeet Dec 05 '12 at 22:08
  • Seems like wise practice. Thanks for the explanation. – Justin Morgan - On strike Dec 07 '12 at 15:20