Contract.Ensures and Exception Handling

Question

I recently discovered the .NET Contracts API, and, although I don't like the way of implementation using methods and not an extended syntax (Sing# did it right, in my opinion), I prefer using them over the old / regular way using if's for e.g. null-checking.

I'm also approaching my first Contract.Ensures-calls and I stumbled over the question how we would deal with Exceptions in a method containing a Contract.Ensures that suffered from an exception while running?

The word Contract.Ensures kinda feels like I have to handle the exceptions inside the method and get my class into correct state again, but what if I couldn't?

Let's say we have this class here:

public class PluginManager
{
    private ILoadedFromAtCompileTimeUnknownAssembly extension;

    public bool IsFinished { get; private set; }

    public void Finish()
    {
        extension.Finish();
        this.IsFinished = true;
    }
}

can we use Contract.Ensures to ensure IsFinished is true after the method completed?

Answer 1

Yes. Ensures basically means "Ensures if the method terminates normally", i.e. without exceptions.

Answer 2

I find it very hard to get the concept of code contracts right. Code Contracts are meant to find programming errors. If applied that way you can remove the contracts of your release build and your application will continue to work perfectly.

BUT it is very hard to distinguish programming (aka logic errors) from configuration and input data issues. These checks must remain in your release builds. It is therefore a bad idea to use Code Contracts to check if an extension/plugin did correctly load because it is usually configured into your application. If you remove the contracts in your release build you get differerent behaviour of your application depending if you configure your app wrong in debug or release builds.

Contract violations are reported with only one exception type which makes it impossible to react in upper layers of your application to e.g. a configuration issue or a logic bug in your application. With react I do not mean to continue but to present a remotely useful message to the user/developer what went wrong.

Code Contract do look nice at the surface but I fear that most people use it in the wrong way. It is not meant to replace all of your null checks for input validation in your methods. You should replace only from the methods the null checks with code contracts where your are sure that a logic problem an not the input data is the root cause.

If you expect a file name in your e.g. console application as input and the the user did forget to supply the file name at the command line it is not a good idea to the greet the user with a ContracException.

• The error message would be confusing to the user.
• You cannot differentate programming errors from user input validation issues.
• You cannot catch any specific ContractException because the exception type is internal.

See user documentation.

7.6 ContractException The ContractException type is not a public type and is emitted as a nested private type into each assembly for which runtime contract checking is enabled. It is thus not possible to write catch handlers catching only ContractException . Contract exceptions can thus only be handled as part of a general exception backstop. The rationale for this design is that programs should not contain control logic that depends on contract failures, just like programs should not catch ArgumentNullException or similar validation exceptions.