CodeContracts - 误报

Question

我刚刚开始在现有的中型项目上尝试 .NET 4 中的 CodeContracts，令我惊讶的是静态检查器向我发出有关以下代码片段的编译时警告：

public class Foo
{
   private readonly List<string> strs = new List<string>();

   public void DoSomething()
   {
       // Compiler warning from the static checker:
       // "requires unproven: source != null"
       strs.Add("hello");
   }
}

Why is the CodeContracts static checker 抱怨关于 strs.Add(...) 行？ strs 不可能为空，对吧？我做错了什么吗？

Answer 1

该字段可能被标记为只读，但不幸的是静态检查器对此不够智能。因此，由于静态检查器无法自行推断 strs 永远不会为 null，因此您必须通过不变量显式地告诉它：

[ContractInvariantMethod]
private void ObjectInvariant() {
    Contract.Invariant(strs != null);
}

Answer 2

以下是有效的代码，我希望它会生成警告。

public class Foo 
{ 
   private readonly List<string> strs = new List<string>(); 

   public Foo()
   {
       // strs is readonly, so we can assign it here but nowhere else
       strs = ResultOfSomeFunction();
   }

   public void DoSomething() 
   { 
       // Compiler warning from the static checker: 
       // "requires unproven: source != null" 
       strs.Add("hello"); 
   } 
}

他们的分析器很可能无法确保构造函数中没有任何内容会更改 strs 的值。或者也许您正在以某种方式更改构造函数中的 strs 而您没有意识到。

Answer 3

小修正：Pex 使用 Z3（一种 SMT 求解器），而 Clousot（静态检查器代码名称）使用抽象解释和抽象域。

Answer 4

我对 .NET 对象初始化语义的复杂性了解不够，无法回答您的直接问题。不过，这里有两个提示：

1. Microsoft Research 的 Pex 可以自动生成单元测试，准确演示在什么情况下可能发生违反合同的情况。它使用与 CC 相同的定理证明器和静态分析器，所以这是一个公平的赌注，两者都会同意。
2. 证明合约相当于解决停止问题，因此仅仅因为 CC 无法证明它永远不会为空，并不意味着它不是真的。 IOW：CC 可能是错误的，您需要使用 Contract.Assume 来帮助它（或者，如果您有信心，可以使用 Contract.Assert）。

有趣的是，如果您显式添加对象不变断言，即 strs 永远不会为 null，CC 能够证明这一点 因此，还可以证明 strs.Add() 永远不会是空引用：

[ContractInvariantMethod]
private void StrsIsNotNull()
{
    Contract.Invariant(strs != null);
}

所以，我想我的预感 #2 是正确的：CC 在这种情况下只是完全错误的。 （或者更准确地说：C# 语义到定理证明者中的编码是不完整的。）