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