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.