c# - CodeContract 认为分配的只读字段可以为空

Question

我有这个代码:

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 给出了这个警告:

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

如果我取消中间行的注释，它就会停止提示。但为什么它一开始就提示呢？ _items 永远不应该为 null..？

Answer 1

合约不是100%，理解上还有差距。

你是对的:没有理由不证明结果。参见 http://social.msdn.microsoft.com/Forums/en-US/codecontracts/thread/f82aa25c-e858-4809-bc21-0a08de260bf1有关此特定问题的更多信息。

目前，您可以使用以下方法解决此问题:

Contract.Assume(_items != null);

您还可以使用契约不变量来实现这一点:

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