Should Contract.Ensures be used in finalizers and Dispose methods?

Question

I read here that invariants are not checked for object finalizers or for any methods that implement the Dispose method, but it doesn't state the reason. I suspect the reason is that invariant conditions may no longer hold true when the object is being disposed, thus potentially making the finalizer or dispose method fail.

If my reasoning is correct, does that mean that I should not use Contract.Ensures() in finalizers and dispose methods (or any code contracts for that matter)?

My specific example is using Contract.Ensures() to ensure that an IsDisposed property is true on exiting a Dispose() method.

public class ExampleClass : IDisposable
{
    public bool IsDisposed { get; set; }

    ~SomeClass()
    {
        Dispose(false);
    }

    public void Dispose()
    {
        Contract.Ensures(IsDisposed);
        Dispose(true);
        GC.SuppressFinalize(this);
    }

    protected virtual void Dispose(bool disposing)
    {
        Contract.Ensures(IsDisposed);
        if (!IsDisposed)
        {
            if (disposing)
            {
                // Other code here
            }
            IsDisposed = true;
        }
    }
}

Answer 1

You can and should use Ensures in your Dispose and finalizer methods. These are applied to your code. Invariants are not applied, because as you say, a finalizer/Dispose method often makes an object invalid in a way that does no longer satisfy the object invariant.