1

私は Design by Contract の概念にかなり慣れていませんが、今のところ、潜在的なバグを簡単に見つけられる点が気に入っています。

ただし、Microsoft.Contracts ライブラリ (これは非常に優れています) を使用して作業しており、障害に遭遇しました。

私がやろうとしていることのこの単純化された例を見てください:

public enum State { NotReady, Ready }

[ContractClass(typeof(IPluginContract))]
public interface IPlugin
{
    State State { get; }
    void Reset();
    void Prepare();
    void Run();
}

[ContractClassFor(typeof(IPlugin))]
public class IPluginContract : IPlugin
{
    State IPlugin.State { get { throw new NotImplementedException(); } }

    void IPlugin.Reset()
    {
        Contract.Ensures(((IPlugin)this).State == State.NotReady);
    }

    void IPlugin.Prepare()
    {
        Contract.Ensures(((IPlugin)this).State == State.Ready);
    }

    void IPlugin.Run()
    {
        Contract.Requires(((IPlugin)this).State == State.Ready);
    }
}

class MyAwesomePlugin : IPlugin
{
    private State state = State.NotReady;

    private int? number = null;

    State IPlugin.State
    {
        get { return this.state; }
    }

    void IPlugin.Reset()
    {
        this.number = null;
        this.state = State.NotReady;
    }

    void IPlugin.Prepare()
    {
        this.number = 10;
        this.state = State.Ready;
    }

    void IPlugin.Run()
    {
        Console.WriteLine("Number * 2 = " + (this.number * 2));
    }
}

要約すると、プラグインが従うインターフェイスを宣言し、状態を宣言するように要求し、任意の状態で呼び出すことができるものを制限しています。

これは、静的検証とランタイム検証の両方で、呼び出しサイトで機能します。Resetしかし、私が得続ける警告は、関数と関数の両方に対して「契約：証明されていないことを保証します」ですPrepare。

私は s を試してみましたが、制約Invariantを証明するのに役立つとは思われません。Ensures

インターフェイスを介して証明する方法についてのヘルプは役に立ちます。

EDIT1：

これを MyAwesomePlugin クラスに追加すると:

    [ContractInvariantMethod]
    protected void ObjectInvariant()
    {
        Contract.Invariant(((IPlugin)this).State == this.state);
    }

IPlugin としての状態が私のプライベート状態と同じであることをほのめかそうとすると、同じ警告が表示され、さらに「private int? number = null」行が不変条件を証明できないという警告が表示されます。

それが静的コンストラクターの最初の実行可能行であることを考えると、なぜそう言うのかがわかりますが、それが ? を証明しないのはなぜEnsuresですか?

EDIT2

でマークStateする[ContractPublicPropertyName("State")] と、「'MyNamespace.State' 型の 'State' という名前のパブリック フィールド/プロパティが見つかりません」というエラーが表示されます。

これは私をより近づけるはずですが、私はまだそこにいません。

4

1 に答える 1

1

このコードスニペットを使用して、警告を効果的に抑制しました。

    void IPlugin.Reset()
    {
        this.number = null;
        this.state = State.NotReady;
        Contract.Assume(((IPlugin)this).State == this.state);
    }

これは実際に私の最初の質問に答えますが、新しい質問をします：なぜ不変の助けがこれを証明しなかったのですか？

新しい質問を投稿します。

于 2009-08-01T16:51:21.397 に答える