Правило языка

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

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

К счастью, возможно простое техническое решение. Нужное нам правило можно сформулировать через простое лингвистическое соглашение, основанное на том наблюдении, что для любых утверждений 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) , хотя запись утверждений в программе (а также, вероятно, их расчет во время выполнения при отсутствии средств символьных преобразований) является более сложной.