按合同设计：您可以使用协议接口吗？ [英] Design by Contract: Can you have an Interface with a Protocol?

问题描述

我对按合同设计的概念还很陌生，但到目前为止，我很喜欢它使发现潜在错误的难易程度。

I'm pretty new to the concept of Design by Contract, but so far, I'm loving how easy it makes it to find potential bugs.

但是，我一直在使用Microsoft.Contracts库（非常棒），并且遇到了障碍。

However, I've been working with the Microsoft.Contracts library (which is pretty great,) and I have run into a road block.

以这个简化的示例说明一下我正在尝试做：

Take this simplified example of what I'm trying to do:

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));
    }
}

总而言之，我声明一个接口插件，然后要求它们声明其状态，并限制在任何状态下都可以调用的插件。

To sum it up, I am declaring an interface for plugins to follow, and requiring them to declare their state, and limiting what can be called in any state.

这在调用站点有效，适用于静态和运行时验证。但是我不断收到的警告是 Reset 和 Prepare 函数的合同：确保未经验证。

This works at the call site, for both static and runtime validation. But the warning I keep getting is "contracts: ensures unproven" for both the Reset and Prepare functions.

我尝试使用 Invariant s进行整形，但这并不能帮助证明确保约束。

I have tried finagling with Invariants, but that doesn't seen to aid in proving the Ensures constraint.

任何有关如何通过界面证明的帮助都将有所帮助。

Any help as to how to prove through the interface would be helpful.

EDIT1：

当我将其添加到MyAwesomePlugin类中时：

When I add this to the MyAwesomePlugin class:

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

试图暗示作为IPlugin的状态与我的私有状态相同，我得到相同的警告，并且警告 private int？number = null行无法证明不变。

Attempting to imply that the state as an IPlugin is the same as my private state, I get the same warnings, AND a warning that the "private int? number = null" line fails to prove the invariant.

鉴于这是第一条可执行行在静态构造函数中，我可以看到为什么会这样说，但是为什么不能证明 Ensures ？

Given that that is the first executable line in the static constructor I can see why it may say so, but why doesn't that prove the Ensures?

EDIT2

当我将 State 标记为 [ContractPublicPropertyName （ State）] 我收到一条错误消息，说找不到名为'MyNamespace.State'类型的名为'State'的公共字段/财产

When I mark State with [ContractPublicPropertyName("State")] I get an error saying that "no public field/property named 'State' with type 'MyNamespace.State' can be found"

似乎应该把我拉近一些，但我还不太远。

Seems like this should put me closer, but I'm not quite there.

推荐答案

使用此代码段，我有效地取消了警告：

With this code snippet, I effectively suppressed the warning:

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

这实际上回答了我的第一个问题，但又提出了一个新问题：为什么没有？不变的帮助证明了这一点？

This actually answers my first question, but asks a new one: Why didn't the invariant help prove this?

我将发布一个新问题。

这篇关于按合同设计：您可以使用协议接口吗？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！