5

我刚刚开始在一个现有的中型项目上使用 .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");
   }
}

为什么 CodeContracts 静态检查器抱怨 strs.Add(...) 行？strs 不可能为空，对吧？难道我做错了什么？

4

4 回答 4

8

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

[ContractInvariantMethod]
private void ObjectInvariant() {
    Contract.Invariant(strs != null);
}
于 2010-08-14T19:40:45.737 回答
3

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

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在构造函数中进行更改而您没有意识到这一点。

于 2010-08-14T19:28:39.977 回答
1

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

于 2010-08-15T14:56:50.093 回答
0

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

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

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

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

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

于 2010-08-14T19:07:54.210 回答