1

我对按合同设计的概念还很陌生，但到目前为止，我很喜欢它让查找潜在错误变得多么容易。

但是，我一直在使用 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功能。

我曾尝试使用Invariants 进行处理，但这并不能帮助证明Ensures约束。

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

编辑1：

当我将此添加到 MyAwesomePlugin 类时：

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

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

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

编辑2

当我标记State时，[ContractPublicPropertyName("State")] 我收到一条错误消息，提示“找不到名为 'State' 且类型为 'MyNamespace.State' 的公共字段/属性”

似乎这应该让我更接近，但我并不完全在那里。

4

1 回答 1

1

使用此代码片段，我有效地抑制了警告：

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

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

我将发布一个新问题。

于 2009-08-01T16:51:21.397 回答