Императив и аппликатив (применимость)

Императив и аппликатив (применимость)

Утверждения из STACK2 иллюстрируют фундаментальную концепцию - разницу между императивным и аппликативным видением.

Утверждения empty и full могут вызвать удивление. Приведу еще раз текст full:

full: BOOLEAN is

-- Заполнен ли стек?

do

Result := (count = capacity)

ensure

full_definition: Result = (count = capacity)

end

Постусловие говорит, что Result имеет значение выражения (count = capacity). Но оператор присваивания именно это значение присваивает переменой Result. В чем же смысл написания постусловия? Не является ли оно избыточным?

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

Инструкция предписывает (prescriptive), утверждение описывает (descriptive). Инструкция описывает "как", утверждение описывает "что". Инструкция является частью реализации, утверждение - элементом спецификации.

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

[x]. Компьютерные операции могут изменять состояние аппаратно-программной машины. Инструкции в языках программирования являются командами (императивные конструкции), заставляющие машину выполнять такие операции.

[x]. Математические вычисления никогда ничего не меняют. Как отмечалось при рассмотрении АТД, взятие квадратного корня от числа 2 не меняет это число. Вместо этого математики описывают как, используя свойства одних объектов, вывести свойства других, таких как v2, полученных применением (applying - отсюда и термин "аппликативный") математических трансформаций.

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

Причина близости нотаций в том, что присваивание зачастую кратчайший путь достижения эквивалентности. Но при переходе к более сложным примерам концептуальное различие между спецификацией и реализацией будет только возрастать. Даже в простейшем случае вычисления квадратного корня постусловие может быть задано в форме: abs(Result^2 -x) <= tolerance, где abs - обозначает абсолютное значение, а tolerance - допустимое отклонение от точного значения. Инструкции, вычисляющие квадратный корень, могут быть не тривиальными, реализуя определенный алгоритм вычисления квадратного корня.

Даже для put в классе STACK2 одной и той же спецификации могут соответствовать различные алгоритмы, например:

if count = capacity then Result := True else Result := False end

или упрощенный вариант, учитывающий правила инициализации:

if count = capacity then Result := True end

В ходе работы мы столкнулись со свойством утверждений, заслуживающим дальнейшей проработки: оно важно для авторов клиентских классов, не интересующихся реализацией, но нуждающихся в абстрактном описании роли программы. Эта идея приведет нас к понятию краткой формы (short form), обсуждаемой далее в этой лекции в качестве основного механизма документирования класса.

Предупреждение: по практическим соображениям допускается включение в утверждение функций - по внешнему виду императивных элементов. Эта проблема исследуется в конце этой лекции.

В заключение обсуждения полезно перечислить слова, используемые по контрасту в двух категориях программных элементов:

Таблица 11.2.Императивно - аппликативное противопоставление