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 吗..？

- Allrameest

Answer 1

合同并非百分之百准确，仍存在理解上的差距。

您是正确的：结果未经证明是没有理由的。请参见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);
}

- Pieter van Ginkel

---

不错，这在我的单元测试中也很有用... :) - Allrameest

更加简洁的解决方法是使用不变量，像这样：[ContractInvariantMethod] void Invariants() { Contract.Invariant(_items != null); }。否则，你需要在各个地方都进行假设 :) - porges

Answer 2

其实我可以想象到这个：

CodeContractSample s = new CodeContractSample();
s.GetType().GetField("_items", BindingFlags.NonPublic | BindingFlags.Instance).SetValue(s, null);
var q = s.Query();

你觉得呢？

- ZFE

---

是的，这种情况可能会发生。但是在运行时，合同将抛出异常。当使用反射进行操作时，我不能再期望静态编译时检查器会给我警告。 - Allrameest

Answer 3

你为什么认为items永远不会是null？你可能在该类中有另一个方法将其设置为null...

- blowdart

---

它是只读的。只有构造函数可以将其设置为空。但我没有任何构造函数。 - Allrameest

Answer 4

Contract.Ensures这一行承诺该方法永远不会返回null。但是在取消注释之前，代码中没有任何防止这种情况发生的措施。

- Jack Allan

---

除了 _items 在类构造函数中被初始化以外，Query 是一个非静态方法。 - fearofawhackplanet

我认为这种功能尚未实现。这将需要对C#语言进行更改。请参见http://channel9.msdn.com/Forums/TechOff/494357-Design-by-Contract-in-C/0ef9306b38314b1aa4c09deb0009144e。 - Jack Allan