代码约定对引用类型和空引用的静态检查

Question

Code Contracts 静态分析是否无法检查单个分支方法（没有任何条件且只有一个 return 的方法）中的显式 return new ...，如：

static public Tuple<int> Foo()
{
    return new Tuple<int>(42);
}

仍然用

警告我

warning : CodeContracts: Possibly calling a method on a null reference. Do you expect that SomeClassName.Foo() returns non-null?

我确实可以帮助静态检查器

Contract.Ensures(Contract.Result<Tuple<int>>() != null);

明确但看起来开销很大。

所以我的问题是：我是不是遗漏了什么，或者这是我对 Ensure 即使是这样微不足道的案件的义务？

Answer 1

调用其他方法时，代码契约依赖于已明确声明的内容。正如您所建议的，在某些情况下它可能会解决这个问题，但总的来说，您真的想要吗？对于像这样的简单示例，它确实有意义，但总的来说，仅仅因为方法当前不 return null 并不意味着作者明确保证了这一点。

这就是合同的用武之地，它不仅描述了代码的作用，还描述了您保证代码将执行的操作，这是一个略有不同的事情。因此，要回答您的问题，是的，即使对于琐碎的案例来说有点开销，您也必须 Ensure 这些琐碎的案例。

Code contracts static checks for reference types and null reference