Дизайн по контракту: можете ли вы иметь интерфейс с протоколом?

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 ограничение.

Любая помощь в том, как доказать через интерфейс будет полезна.

EDIT1:

Когда я добавляю это в класс MyAwesomePlugin:

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

Пытаясь предположить, что состояние IPlugin совпадает с моим личным состоянием, я получаю те же предупреждения и предупреждение о том, что строка "private int? Number = null" не может доказать инвариант.

Учитывая, что это первая исполняемая строка в статическом конструкторе, я могу понять, почему он может так сказать, но почему это не доказывает Ensures?

EDIT2

Когда я отмечаю State с [ContractPublicPropertyName("State")] Я получаю сообщение об ошибке, в котором говорится, что "не найдено открытого поля / свойства с именем" State "с типом" MyNamespace.State ""

Похоже, это должно приблизить меня, но я не совсем там.

Answer 1

С помощью этого фрагмента кода я эффективно подавил предупреждение:

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

Это фактически отвечает на мой первый вопрос, но спрашивает новый: почему инвариант не помог доказать это?

Я буду публиковать новый вопрос.