7

CodeContracts 静的解析ツールと議論しています。

私のコード:

スクリーンショット

(アスキー版)

ツールはinstance.bar、null 参照である可能性があることを示しています。私は反対のことを信じています。

誰が正しいですか？どうすればそれが間違っていると証明できますか?

4

5 に答える 5

2

CodeContracts は正しいです。instance.bar = nullメソッドを呼び出す前に設定することを妨げるものは何もありませんBarLength()。

于 2010-04-20T23:29:45.053 に答える
2

更新: 問題は、静的フィールドで不変条件がサポートされていないことです。

2 回目の更新:以下に概説する方法は、現在推奨される解決策です。

考えられる回避策は、保持したい不変条件のプロパティを作成するinstanceことです。Ensure(もちろん、 を証明するにAssumeはそれらが必要Ensureです。) これが完了したら、プロパティを使用するだけで、すべての不変条件が正​​しく証明されるはずです。

このメソッドを使用した例を次に示します。

class Foo
{
    private static readonly Foo instance = new Foo();
    private readonly string bar;

    public static Foo Instance
    // workaround for not being able to put invariants on static fields
    {
        get
        {
            Contract.Ensures(Contract.Result<Foo>() != null);
            Contract.Ensures(Contract.Result<Foo>().bar != null);

            Contract.Assume(instance.bar != null);
            return instance;
        }
    }

    public Foo()
    {
        Contract.Ensures(bar != null);
        bar = "Hello world!";
    }

    public static int BarLength()
    {
        Contract.Assert(Instance != null);
        Contract.Assert(Instance.bar != null);
        // both of these are proven ok

        return Instance.bar.Length;
    }
}
于 2010-05-05T23:14:06.733 に答える
2

コードには、プライベートな静的初期化インスタンスが含まれています。

private static Foo instance = new Foo();

これは、静的メソッドにアクセスする前にインスタンスコンストラクターが常に実行されることを意味するため、確実に初期化されると想定しbarていますか?

シングルスレッドの場合、私はあなたが正しいと思います。

イベントのシーケンスは次のようになります。

  1. に呼び出しますFoo.BarLength()
  2. クラスの静的初期化Foo(まだ完了していない場合)
  3. instanceのインスタンスを使用したプライベート静的メンバーの静的初期化Foo
  4. へのエントリーFoo.BarLength()

ただし、クラスの静的初期化はアプリ ドメインごとに 1 回だけトリガーされます。また、IIRC では、他の静的メソッドが呼び出される前に完了することを保証するブロックはありません。

したがって、次のシナリオが考えられます。

  1. スレッド アルファ: への呼び出しFoo.BarLength()
  2. Thread Alpha: クラスの静的初期化Foo(まだ完了していない場合) が開始されます
  3. コンテキスト スイッチ
  4. スレッド ベータ: への呼び出しFoo.BarLength()
  5. スレッド ベータ:既に進行中のため、クラスの静的初期化への呼び出しはありませんFoo
  6. スレッドベータ: エントリーFoo.BarLength()
  7. nullスレッド ベータ:静的メンバーへのアクセスinstance

コントラクト アナライザーは、コードをマルチスレッドで実行したことがないということを知ることはできないため、慎重に行う必要があります。

于 2010-04-21T01:15:47.297 に答える
0

フィールド「バー」を読み取り専用としてマークすると、静的アナライザーは、ctor の実行後にフィールドが他の値に設定されないことを確認する必要があります。

于 2010-04-21T00:52:44.003 に答える
-1

仰るとおりです。 instanceとbar両方とも非公開であるため、CodeContracts は がinstance.barnull に設定されていないことを認識できるはずです。

于 2010-04-20T23:36:22.070 に答える