This post will deal with the Contract.ValueAtReturn() method of the Microsoft Code Contracts. The method enables the contract to specify post conditions on out parameters. Where the Contract.Result is used to get a peek at the final return value, the Contract.ValueAtReturn does almost the same thing on out parameters.

To make it a bit more clear, I created a simple example:

    public bool TestingOutParameter(int x, out int y)
    {
      Contract.Ensures(!Contract.Result<bool>() ?
                       Contract.ValueAtReturn<int>(out y) == -1 :
                       Contract.ValueAtReturn(out y) == x + 1);
 
      if (x == int.MaxValue)
      {
        y = -1;
        return false;
      }
 
      y = x + 1;
      return true;
    }

This tests the incoming parameter x, when it is int.MaxValue, the method will return false and y will have the value of -1, otherwise it will return true and y will equal x + 1. Please note that in the example I have included the type int in the first call, but not in the second. It would not have been necessary to put it in either call, since the compiler would have inferred the type from the usage anyway. I included it to show that it could be used in both ways. However, if the type can not be inferred, it MUST be stated and can not be omitted.

Just like the Contract.OldValue the method can only be used in a Contract.Ensures call. And speaking of post conditions, there is just one call left to deal with in that part. And that is the Contract.EnsuresOnThrow call. And that will be the subject of the next post in this series.

That’s it for now
Meile