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

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

1 голос
/ 01 августа 2009

Я довольно новичок в концепции проектирования по контракту, но пока мне нравится, как легко можно найти потенциальные ошибки.

Однако я работал с MicrosoftБиблиотека контрактов (что довольно здорово), и я столкнулся с дорожным блоком.

Возьмите этот упрощенный пример того, что я пытаюсь сделать: 

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")], я получаю сообщение об ошибке, в котором говорится, что «никакое открытое поле / свойство с именем« State »с типом« MyNamespace.State »не можетбыть найденным "

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

1 Ответ

1 голос
/ 01 августа 2009

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

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

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

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

...