Have to prove base class property invariant in all derived classes?

Question

I have a base class in which I'm trying to use the Null Object pattern to provide a default logger implementation which can then be changed by IoC setter injection at a later stage.

public interface ILog
{
    void Log(string message);
}

public class NoOpLogger: ILog 
{
    public void Log(string message)
    { }
}

public abstract class ClassWithLogger
{
    private ILog _logger = new NoOpLogger();

    protected ClassWithLogger()
    {
        Contract.Assert(Logger != null);
    }

    public ILog Logger
    {
        get { return _logger; }
        set
        {
            Contract.Requires(value != null);
            _logger = value;
            Contract.Assert(Logger != null);
        }
    }

    [ContractInvariantMethod]
    private void ObjectInvariant()
    {
        Contract.Invariant(Logger != null);
    }
}

public sealed class DerivedClass : ClassWithLogger
{
    private readonly string _test;
    public DerivedClass(string test)
    {
        Contract.Requires<ArgumentException>(!String.IsNullOrWhiteSpace(test));
        _test = test;

        // I get warning at end of ctor: "invariant unproven: Logger != null"
    }

    public void SomeMethod()
    {
        Logger.Log("blah");
    }
}

As I indicate in the code, my issue is that I get a warning at the end of the derived class' constructor saying that the "Logger != null" object invariant from the base class has not been proven even though it's obvious nothing has changed the Logger property value and I also have contracts around the setter to ensure it can never be null anyway.

Is there any way to avoid having to reprove this fact in all derived classes, or is this just a limitation of the static analyser?

UPDATE: Problem has been fixed in latest version of CodeContracts. Also, I don't need the assert in the abstract base class constructor anymore (the line "Contract.Assert(Logger != null);")

Answer 1

I just tested your code as posted and it worked fine. Are you using the most recent version of Code Contracts (1.4.30707.2)?