契約による設計：プロトコルとのインターフェースがありますか？

Question

私はContract by Designのコンセプトをかなり新しくしていますが、これまでのところ、バグを見つけ出すのがとても簡単です。

しかし、私は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の両方の機能について、「契約：保証されていないことを保証する」ことです。

私はInvariantで細工しようとしましたが、それはEnsuresという制約の証明には役立たないと考えられます。

インターフェイスを介してどのように証明するかについての助けが役に立ちます。

EDIT1：私はこれがMyAwesomePluginクラスに追加すると

は：

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

IPluginような状態は私のプライベート状態と同じであることを暗示しようとすると、私は同じ警告を取得、および "private int？number = null"行が不変量を証明できないという警告が表示されます。

静的なコンストラクタの最初の実行可能な行であることから、私はなぜそれがそうだと言えるのか理解できますが、それはなぜEnsuresを証明していませんか？

私は「何が公共の場/タイプ 『MyNamespace.State』と 『国家』という名前のプロパティを見つけることができる」

はのように思えることを言っていないエラーを取得し[ContractPublicPropertyName("State")]とStateをマーク

EDIT2これは私を近づけるはずですが、私はそこにはあまりありません。このコードスニペットで

Answer 1

が、私は効果的に警告を抑制：

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

これは実際に私の最初の質問に答えるが、新しいものを尋ねる：なぜ不変のヘルプはこれを証明しませんでしたか？

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