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

Булевы выражения не ограничиваются использованием атрибутов и локальных сущностей. Мы уже использовали возможность вызова функций в утверждениях: предусловие для put класса стек было not full, где full - функция

full: BOOLEAN is

-- Is stack full? (Заполнен ли стек?)

do

Result := (count = capacity)

ensure

full_definition: Result = (count = capacity)

end

В этом наш маленький секрет, - мы вышли из рамок исчисления высказываний, в котором булевы выражения могут строиться только из переменных, констант и знаков логических операций. Благодаря введению функций, мы получили мощный механизм, позволяющий вычислять булевы значения любым, подходящим для нас способом. Не следует беспокоиться о присутствии постусловия самой функции full , это не создает никакого пагубного зацикливания. Детали вскоре.

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

index_not_too_small: lower <= i

index_not_too_large: i <= upper

одним предложением в форме

index_in_bounds: correct_index (i)

с определением функции

correct_index (i: INTEGER): BOOLEAN is

-- Является ли i внутри границ массива?

do

Result := (i >= lower) and (i <= upper)

ensure

definition: Result = ((i >= lower) and (i <= upper))

end

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

-- Result является максимумом нарезки массива t в интервале [t.lower,i]

формально может быть выражен так

Result = (t.slice (lower, i)).max

в предположении, что slice вырабатывает нарезку - массив с индексами от lower до i , - а функция max дает максимальный элемент этого массива.

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

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

[x].Включение полного языка спецификаций, как отмечалось, приводит к потере эффективности и простоты изучения.

[x].Вероятно, хуже то, что неясно, достаточны ли общепринятые языки утверждений. Возьмем, например, такого естественного кандидата, в которого многие верят, - язык логики предикатов первого порядка. Этот формализм не позволяет нам выразить некоторые свойства, представляющие непосредственный интерес для разработчиков и часто используемые в утверждениях, такие как, например, "граф не имеет циклов" (типичный инвариант цикла). Математически это может быть выражено как r + , где r - это отношение на графе, а + его транзитивное замыкание. Хотя можно представить себе язык спецификации, поддерживающий эти понятия, большинство языков этого не делают.

Все это создает больше трудностей для программиста, которому проще написать булеву функцию cyclic , исследующую граф и возвращающую true , если и только если в графе есть цикл. Такие примеры являются серьезными аргументами в пользу базисного языка утверждений с использованием функций для повышения его выразительной силы.