This is the first post that will be about post conditions. So far, I’ve tried to shred some light on defining preconditions with the help of the Code Contracts that are now part of the .NET framework since version 4. In the past, preconditions could and would be defined with the help of the IF-THEN-THROW construction. For a broader explanation on that, see my previous post in this series.

Now I’ll move on to post conditions. I have not often included post conditions in my code. Of course you would design your code to never return a null value, of that would be a requirement. But how would you go about checking that? A possible construction would be the following:

    public int Process()
    {
      var processable = from p in this.currentList
                        where p.Processable
                        select p;
 
      int result = processable.Count();
 
      // process the bunch....
 
      if (result != processable.Count())
      {
        throw new Exception("Count does not match number of processed items");
      }
 
      return result;
    }

The code above has some points to be cautious about. For instance, the value in the variable that is returned might have been changed on a different thread, before it is returned by the method body. How would you verify that? That would not be easy, especially not when your code is not as succinct as it could be and probably has dependencies you were not even aware of. Of course the code above contains a major flaw, since it uses a LINQ query to determine the count of items. But would every developer be aware of this?

Luckily now there is the Contract.Ensures method to the rescue. As I’ve stated before, there is no ‘silver bullet’, and this one is no exception. It does not end all bugs in your code, but it goes a long way. The binary rewriter would make sure the code is checked at the end of the method. But that’s something you could implement yourself. However, the static checker goes the other mile, by checking what you’ve stated must be true. And in the above example, if it were written with the use of Contract.Ensures, the checker would warn you about the fact that the currentList’s entries may have their Processable property changed and therefore it can not verify the correctness of your post condition.

Now back to our main example targeted also in our previous posts. Rewritten with the help of the Contract.Ensures method it will become like this:

    public string RepeatFirstCharacter(string input, int count)
    {
      Contract.Requires<ArgumentNullException>(input != null);
      Contract.Requires<ArgumentException>(input.Length >= 0, "The input should have at least one character.");
      Contract.Requires<ArgumentOutOfRangeException>(count > 0);
      Contract.Ensures(Contract.Result<string>().Length == count);
 
      return new string(input.ToCharArray(0, 1)[0], count);
    }

This verifies that the length of the returned string value is equal to the int count parameter. An additional check could be the following:

      Contract.Ensures(Contract.ForAll<char>(Contract.Result<string>().ToCharArray(), p => p == input[0]));

This verifies that result only contains the first character of the string input parameter. You may have been wondering what this construction Contract.Result<> is used for. Well, that will be the topic of the next post in this series. And the Contract.ForAll<> will follow in another post as well. Just stay tuned.

That’s it for now.
Meile