In previous post I dabbled about the post conditions using the Contract.Ensures method. But what if the method body throws an exception? Or any called method throws? How would you ensure certain state without the Code Contracts? Probably using some try-finally construction or just a try-catch. But as with other conditions, pre and post, the try-finally and try-catch will only have impact on the current enclosing method body, and not on any derived or overridden one.
With the help of the Contract.EnsuresOnThrow<TException> this gets a little bit easier. It will ensure the post condition not only on the current enclosing method body, but also on any derived and overridden member. Let look at an example:
public bool AddAndProcessItem(T item)
{
Contract.Requires(item != null);
Contract.Ensures(this.Count == Contract.OldValue<int>(this.Count) + 1);
Contract.EnsuresOnThrow<DbException>(!item.IsProcessed);
try
{
// do processing here which may throw a DbException...
}
catch (DbException)
{
item.IsProcessed = false;
throw;
}
this.innerList.Add(item);
return true;
}
Here the post condition ensures that on a DbExeption being thrown the item’s IsProcessed property will have the value false. The example shown here catches a possible thrown DbException, sets the state property and lets the exception propagate to a higher level. But you could also have code that throws an exception itself, for instance when a certain operation is invalid, you might throw an exception of type InvalidOperationException. If we would have the following just preceding the try-clause:
if (this.innerList.Contains(item))
{
throw new InvalidOperationException("Item cannot be processed when it is already added.");
}
we could add the following post condition:
Contract.EnsuresOnThrow<InvalidOperationException>(item.IsProcessed == Contract.OldValue<T>(item).IsProcessed);
This would ensure that also in case of an InvalidOperationException the IsProcessed value of the item is the same as it was before entering the method. So the method body should not have ‘touched’ this property in case of the InvalidOperationException being thrown.
This concludes the parts about post conditions. In this I discussed the use of Contract.ForAll() already in this post, which is not restricted to use in post conditions, but may be used in preconditions as well. And even beyond those. There is also the Contract.Exists call, which will be the subject of the next post. After that I’ll try to post something useful on Contract.Assume and Contract.Assert. Also the object invariant is still left to discuss, with the Contract.Invariant call. And of course there are still a few attributes to dabble about.
That’s it for now
Meile