按契约设计：你能有一个协议接口吗？

Question

我对契约设计的概念还很陌生，但到目前为止，我很喜欢它让发现潜在错误变得多么容易。

然而，我一直在使用 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 约束。

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

编辑1：

当我将其添加到 MyAwesomePlugin 类时：

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

试图暗示作为 IPlugin 的状态与我的私有状态相同，我收到相同的警告，并且警告“private int? number = null”行未能证明不变式。

鉴于这是静态构造函数中的第一个可执行行，我可以理解为什么它会这么说，但为什么这不能证明 Ensures 呢？

EDIT2

当我用 [ContractPublicPropertyName("State")] 标记 State 时，我收到一条错误消息，指出“没有名为 'State” 的公共字段/属性' 可以找到类型为 'MyNamespace.State' 的内容”

似乎这应该让我更接近，但我还没有完全做到这一点。

Answer 1

通过这个代码片段，我有效地抑制了警告：

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

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

我将发布一个新问题。