Нужны ли предусловия и постусловия в дополнение к инвариантам в функциях-членах при проектировании по контракту?

Question

Я понимаю, что в методе DbC к функции прикрепляются предусловия и постусловия.

Мне интересно, применимо ли это и к функциям-членам.

Например, если я использую инварианты в начале и в конце каждой публичной функции, функция-член будет выглядеть так:

редактировать:(подчистил мой пример)

void Charcoal::LightOnFire() {
  invariant();
  in_LightOnFire();

  StartBurning();    
  m_Status = STATUS_BURNING;
  m_Color = 0xCCCCCC;

  return; // last return in body

  out_LightOnFire();
  invariant();
}

inline void Charcoal::in_LightOnFire() {
  #ifndef _RELEASE_
  assert (m_Status == STATUS_UNLIT);
  assert (m_OnTheGrill == true);
  assert (m_DousedInLighterFluid == true);
  #endif
}

inline void Charcoal::out_LightOnFire() {
  #ifndef _RELEASE_
  assert(m_Status == STATUS_BURNING);
  assert(m_Color == 0xCCCCCC);
  #endif
}

// class invariant
inline void Charcoal::invariant() {
  assert(m_Status == STATUS_UNLIT || m_Status == STATUS_BURNING || m_Status == STATUS_ASHY);
  assert(m_Color == 0x000000 || m_Color == 0xCCCCCC || m_Color == 0xEEEEEE);
}

Можно ли использовать предусловия и постусловия только с глобальными/универсальными функциями и просто использовать инварианты внутри классов?

Это кажется излишним, но, возможно, это мой пример плохой.

редактировать:

Разве постусловие не просто проверяет подмножество инварианта?

Выше я следую инструкциям http://www.digitalmars.com/ctg/contract.html в котором говорится: «Инвариант проверяется при завершении работы конструктора класса, в начале деструктора класса, перед запуском открытого члена и после завершения общедоступной функции».

Спасибо.

Answer 1

Да.

Класс С инвариант является общим свойством всех его экземпляров (объектов).Инвариант оценивается как true тогда и только тогда, когда объект находится в семантически допустимом состоянии.

Инвариант лифта может содержать такую ​​информацию, как ASSERT(IsStopped() || Door.IsClosed()), потому что лифт не может находиться в состоянии, отличном от состояния остановки (скажем, подъема) и с открытой дверью.

Напротив, функция-член, такая как MoveTo(int flat) можно иметь CurrentFlat()==flat как постусловие;потому что после вызова MoveTo(6) текущая квартира равна 6.Точно так же оно может иметь IsStopped() как предварительное условие, потому что (в зависимости от конструкции) вы не можете вызвать функцию MoveTo, если лифт уже движется.Сначала вам нужно запросить его состояние, убедиться, что он остановлен, а затем вызвать функцию.

Конечно, возможно, я слишком упрощаю принцип работы лифта.

В любом случае предусловия и постусловия вообще не будут иметь смысла как инвариантные условия;лифту не обязательно находиться на шестом этаже, чтобы находиться в рабочем состоянии.

Более краткий пример можно найти здесь: Перехват и атрибуты:Образец проекта по контракту от Саши Гольдштейна.

Answer 2

Ограничение контрактов в классах инвариантами не является оптимальным.

Предусловия и постусловия — это не просто подмножество инвариантов.

Инварианты, предусловия и постусловия играют совершенно разные роли.

Инварианты подтверждают внутреннюю связность объекта. Они должны быть действительными в конце конструктора, а также до и после каждого вызова метода.

Предварительные условия проверяют, подходят ли статус объекта и аргументы для выполнения метода. Предусловия дополняют инварианты.Они охватывают проверку аргументов (более строгую проверку, чем сам тип, т.е.не ноль, > 0,..и т. д.), но также может проверять внутренний статус объекта (т.е.вызов file.write("привет") является допустимым вызовом, только если file.is_rw и file.is_open имеют значение true).

Постусловия проверяют, что метод выполнил свои обязательства. Постусловия также дополняют инварианты.Конечно, статус объекта должен быть последовательным после выполнения метода, но постусловия проверяют, было ли выполнено ожидаемое действие (т.е.list.add(i) должен иметь следствием то, что list.has(i) имеет значение true и list.count = old list.count + 1).

Answer 3

Ну, смысл инварианта в том, что он описывает что-то, что истинно для объекта всегда.В данном случае что-то есть на гриле или нет (ничего среднего).Обычно они описывают свойство всего состояния объекта.

Условия до и после описывают вещи, которые истинны непосредственно перед выполнением метода и сразу после него, и будут касаться просто состояние, которого должен был коснуться метод.Это, по-видимому, отличается от состояния объекта.Пред- и пост-условия можно рассматривать как описание следа метода — именно того, что ему нужно, именно того, чего он касается.

Итак, что касается конкретного вопроса, идеи действуют по-разному, поэтому вы вполне можете захотеть и то, и другое.Вы, конечно, не можете просто использовать инварианты вместо пред- и пост-условий — в этом случае частью инварианта объекта является «Что-то есть на гриле или нет», но предварительное условие LightOnFire должно знать, что предмет находится на гриле.Вы никогда не сможете вывести это из инварианта объекта.Это правда, что на основе пред- и постусловий и известного начального состояния вы можете (при условии, что структура объектов изменяема только с помощью методов, а пред- и постусловия описывают все изменения окружающей среды) вывести инвариант объекта.Однако это может быть сложно, и когда вы излагаете вещи «на языке», проще предоставить и то, и другое.

Конечно, делать варианты, в которых логический элемент является либо истинным, либо ложным, немного бессмысленно — система типов гарантирует это.