按合同设计：您可以有一个协议接口吗？

我对合同设计的概念相当陌生，但到目前为止，我非常喜欢它能够轻松找到潜在的错误。但是，我一直在使用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

按合同设计：您可以有一个协议接口吗？

回答

相关问题