按合同設計：您可以有一個協議接口嗎？

我對合同設計的概念相當陌生，但到目前爲止，我非常喜歡它能夠輕鬆找到潛在的錯誤。但是，我一直在使用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 s討價還價，但沒有看到有助於證明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’屬性，可以發現」

好像這應該讓我更接近，但我不是那裏。

來源

2009-07-31 John Gietzen

我想知道是否爲`state`添加`ContractPublicPropertyName`會有幫助。 – 2009-07-31 22:13:06

有了這個代碼片段，我有效地抑制了警告：

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

這實際上回答我的第一個問題，但要求一個新問題：爲什麼沒有不變的幫助下證明這一點？

我會發佈一個新問題。

來源

2009-08-01 16:51:21

按合同設計：您可以有一個協議接口嗎？

回答

相關問題