CodeContract think assigned readonly field can be null

Question

I've got this code:

public class CodeContractSample
{
    private readonly List<object> _items = new List<object>();

    public IEnumerable<object> Query()
    {
        Contract.Ensures(Contract.Result<IEnumerable<object>>() != null);
        //if (_items == null) throw new Exception();
        return _items;
    }
}

CodeContracts gives this warning:

CodeContracts: ensures unproven: Contract.Result>() != null

If I uncomment the middle row it stops complaining. But why does it complain to start with? _items should never be null..?

Answer 1

Contracts are not 100% and there are still gaps in what it understands.

You are right: there is no reason for the result being unproven. See http://social.msdn.microsoft.com/Forums/en-US/codecontracts/thread/f82aa25c-e858-4809-bc21-0a08de260bf1 for more information on this specific issue.

For now, you can solve this using:

Contract.Assume(_items != null);

You can also achieve this using contract invariants:

[ContractInvariantMethod]
void Invariants()
{
    Contract.Invariant(_items != null);
}