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

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

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

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

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

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

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

Это неформальное требование достаточно ясно на практике; формализм подъязыка IFL исключает все императивные элементы, которые либо изменяют глобальное состояние системы, либо не имеют тривиальных аппликативных эквивалентов, в частности исключаются:

[x]. присваивания атрибутам;

[x]. присваивания в циклах;

[x]. вызовы программ, не входящих в IFL.

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

Некоторые технические вопросы могут потребовать внимания. Функция f, используемая в утверждении программы r, может сама иметь утверждения, что демонстрируют примеры функций full и correct_index. Возникает потенциальная проблема при мониторинге утверждений в период выполнения: если при вызове r мы вычисляем утверждение, вызывающее f, то не придется ли нам вычислять утверждение для f? Нетрудно сконструировать пример зацикливания, если пойти по этому пути. Но даже и без этого риска было бы неправильно вычислять утверждение для f. Это бы означало, что мы рассматриваем "на равных" программы, являющиеся предметом наших вычислений, такие как r, и их функции утверждения, такие как f. В противовес этому сформулируем правило, согласно которому утверждения должны иметь более высокий приоритет, чем программы, которые они защищают, их корректность должна быть кристально ясной. Правило простое:

Правило вычисления утверждения

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

Если вызов f встречается как часть проверки утверждения программы r, то слишком поздно спрашивать, удовлетворяет ли f своим утверждениям. Подходящим является время, когда решается вопрос использования f в утверждении, применимом к r.

Рассматривайте f как охранника ядерного предприятия, в обязанности которого входит проверка посетителей. Охранников тоже нужно проверять, но не тогда, когда они сопровождают посетителей.

ОО-модель, разрабатываемая до сих пор, включала два частично не связанных аспекта, оба из которых полезны:

[x]. Понятие инварианта класса, введенное в этой лекции.

[x]. Гибкая модель периода выполнения, детально рассмотренная в начальных лекциях, существенно использующая ссылки.

К несчастью, эти индивидуально желательные свойства могут стать причиной трудностей при их совместном использовании.

Проблема вновь в динамически создаваемых псевдонимах, предохраняющих нас от проверки корректности класса на том основании, что класс делает это сам. Мы уже видели, что корректность класса означает проверку m+n свойств, выражающих следующее (если мы концентрируем внимание на инвариантах INV, игнорируя предусловия и постусловия, не играющие здесь роли):

1 Каждая из m процедур создания порождает объект, удовлетворяющий INV.

2 Каждая из n экспортируемых программ сохраняет INV.