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 が null になる方法はありませんよね？私は何か間違ったことをしていますか？

4

4 に答える 4

8

フィールドは とマークされている可能性がありますreadonlyが、残念ながら静的チェッカーはこれを行うには十分にスマートではありません。したがって、静的チェッカーは null にならないことを独自に推論できないため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 は SMT ソルバーである Z3 を使用し、Clousot (静的チェッカーのコード名) は抽象解釈と抽象ドメインを使用します。

于 2010-08-15T14:56:50.093 に答える
0

あなたの直接の質問に答えるには、.NET のオブジェクト初期化セマンティクスの複雑さに十分な知識がありません。ただし、次の 2 つのヒントがあります。

  1. Microsoft Research の Pexは、契約違反が発生する可能性がある条件を正確に示す単体テストを自動的に生成できます。CC と同じ定理証明器と静的アナライザーを使用しているため、2 つの意見が一致することは間違いありません。
  2. 契約を証明することは、停止問題を解決することと同じであるため、CC がではないことを証明できないからといってnull、それが真実ではないということにはなりません。IOW: CC が間違っている可能性がありContract.AssumeますContract.Assert。

strs興味深いことに、決して にならないObject Invariant Assertion を明示的に追加するとnull、CCはそれを証明でき、その結果、strs.Add()が決して null 参照にならないことも証明できます。

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

したがって、私の推測 #2 は正しいと思います。この場合、CC は単純に間違っています。(より正確には、C# のセマンティクスの定理証明器へのエンコードは不完全です。)

于 2010-08-14T19:07:54.210 に答える