Требуются ли предварительные и постусловия в дополнение к инвариантам в функциях-членах, если проектирование выполняется по контракту?

Question

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

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

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

edit: (убрал мой пример)

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

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

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

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

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

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

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

Answer 2

Да.

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

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

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

Конечно, я могу полностью упростить работу лифта.

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

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

Answer 3

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

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

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

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