Основы объектно-ориентированного программирования

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

К счастью, возможно простое техническое решение. Нужное нам правило можно сформулировать через простое лингвистическое соглашение, основанное на том наблюдении, что для любых утверждений a и b:

[x]. влечет or γ независимо от значения γ;

[x]. β and влечет β независимо от значения .

Итак, гарантируется, что новое предусловие слабее исходного либо равно ему, если оно имеет вид or γ. Гарантируется, что новое постусловие сильнее исходного β либо равно ему, если оно имеет вид β and . Отсюда следует искомое языковое правило:

Правило (2) Утверждения Переобъявления

При повторном объявлении подпрограммы нельзя использовать предложения require или ensure. Вместо них следует использовать предложение, начинающееся с:

[x]. require else, объединенное с исходным предусловием логической связкой or

[x]. ensure then, объединенное с исходным постусловием логической связкой and.

При отсутствии таких предложений действуют исходные утверждения.

Заметим, что используются нестрогие булевы операторы and then и or else, а не обычные and и or, хотя чаще всего это различие несущественно.

Иногда получаемые утверждения могут оказаться сложнее, чем необходимо на самом деле. В примере с подпрограммой обращения матриц, где исходным было утверждение

invert (epsilon: REAL) is

-- Обращение текущей матрицы с точностью epsilon

require

epsilon >= 10 ^ (-6)

...

ensure

((Current * inverse) |-| One) <= epsilon

мы не вправе в повторном объявлении использовать require и ensure, поэтому результат

примет вид

...

require else

epsilon >= 10 ^ (-20)

...

ensure then

((Current * inverse) |-| One) <= (epsilon / 2)

а стало быть, предусловие формально станет таким: (epsilon >= 10 ^ (-20)) or else (epsilon >= 10 ^ (-6)).

Ситуация с постусловием аналогична. Такое расширение не имеет особого значения, поскольку преобладает более слабое предусловие или более сильное постусловие. Если γ влечет , то or else γ имеет то же значение, что и . Если β влечет , то β and then имеет то же значение, что и β. Поэтому математически предусловие повторного объявления есть: epsilon >= 10 ^ (-20), а его постусловие есть: ((Current * inverse) |-| One) <= (epsilon / 2), хотя запись утверждений в программе (а также, вероятно, их расчет во время выполнения при отсутствии средств символьных преобразований) является более сложной.

Повторное объявление функции как атрибута

Правило Утверждения Переобъявления нуждается в небольшом дополнении ввиду возможности при повторном объявлении задать функцию как атрибут. Что произойдет с предусловием функции и ее постусловием, если таковые имелись?

Атрибут доступен всегда, а потому мы вправе считать, что его предусловие равно True. В итоге можно полагать, что предусловие атрибута, согласно правилу Утверждения Переобъявления, было ослаблено.

Но атрибут не имеет постусловий. Мы же должны гарантировать, что он наделен всеми свойствами, заданными исходной функцией. Поэтому (в дополнение к правилу Утверждения Переобъявления) будем считать, что в этом случае автоматически постусловие добавляется к инварианту класса. Плоская форма класса будет содержать это условие в составе своего инварианта.

Для функции без параметров, формулируя некое свойство ее результата, вы всегда можете выбрать, включать ли его в постусловие или в инвариант. С точки зрения стиля предпочтительно пользоваться инвариантом. Соблюдение этого правила позволит отказаться от внесения изменений в утверждения в будущем, если при повторном объявлении функция становится атрибутом.

Замечание математического характера