我有这段代码:
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 吗..?
[ContractInvariantMethod] void Invariants() { Contract.Invariant(_items != null); }
。否则,你需要在各个地方都进行假设 :) - porges