Основы объектно-ориентированного программирования - Бертран Мейер
Шрифт:
Интервал:
Закладка:
Потребуем, чтобы ссылки были связаны содержательным условием. Если ссылка forward определена и задает экземпляр класса В, то ссылка backward этого экземпляра, в свою очередь, должна указывать на соответствующий экземпляр класса А. Это может быть выражено как инвариант класса А:
round_trip: (forward /= Void) implies (forward.backward = Current)
Вот пример ситуации, включающей экземпляры обоих классов и удовлетворяющей инварианту:
Рис. 11.9. Согласованность ссылок forward и backward
Инвариант round_trip встречается в классах довольно часто. Например, в роли класса А может выступать класс PERSON, характеризующий персону. Ссылка forward может указывать в этом случае на владение персоны - объект класса HOUSE. Ссылка backward в этом классе указывает на владельца дома. Еще одним примером может быть реализация динамической структуры - дерева, узел которого содержит ссылки на старшего сына и на родителя. Для этого класса можно ввести инвариант в стиле round_trip:
Предположим, что инвариант класса В, если он есть, ничего не говорит об атрибуте backward. Следующая версия класса А по-прежнему имеет инвариант:
class A feature
forward: B
attach (b1: B) is
-- Ссылка b1 на текущий объект.
do
forward := b1
-- Обновить ссылку backward объекта b1 для согласованности:
if b1 /= Void then
b1.attach (Current)
end
end
invariant
round_trip: (forward /= Void) implies (forward.backward = Current)
end
Вызов b1.attach восстанавливает инвариант после обновления forward. Класс В должен обеспечить свою собственную процедуру attach:
class B feature
backward: B
attach (a1: A) is
-- Ссылка a1 на текущий объект.
do
backward := a1
end
end
Класс А сделал все для своей корректности: процедура создания по умолчанию гарантирует выполнение инварианта, так как устанавливает forward равным void, а его единственная процедура гарантирует истинность инварианта. Но рассмотрим выполнение у клиента следующей программы:
a1: A; b1: B
...
create a1; create b1
a1.attach (b1)
b1.attach (Void)
Вот ситуация после выполнения последней инструкции:
Рис. 11.10. Нарушение инварианта
Инвариант для ОА нарушен. Этот объект теперь указывает на ОВ, но ОВ не указывает на ОА, - backward равно void. Вызов b1.attach мог связать ОВ с любым другим объектом класса А и это тоже было бы некорректно.
Что случилось? Динамические псевдонимы вновь себя проявили. Приведенное доказательство корректности класса А правильно, и единственная процедура этого класса attach спроектирована в полном соответствии с замыслом. Но этого недостаточно для сохранения согласованности ОА, так как свойства ОА могут включать экземпляры других классов, а доказательство ничего не говорит об эффекте, производимом свойствами других классов на инвариант из А.
Эта проблема достаточно важна, и заслуживает собственного имени: Непрямой Эффект Инварианта (Indirect Invariant Effect). Он может возникать сразу же при допущении динамических псевдонимов, благодаря которому операции могут модифицировать объекты даже без включения любой связанной сущности. Но мы уже видели, как много пользы приносят динамические псевдонимы; и схема forward - backward далеко не академический пример, это, как отмечалось, полезный образец для практических приложений и библиотек.
Что можно сделать? Промежуточный ответ включает соглашения для мониторинга утверждений в период выполнения. Вы, возможно, удивлялись, почему эффект включения мониторинга утверждений на уровне assertion (invariant) был описан так:
"Проверка выполнимости инвариантов класса на входе и выходе программы для квалифицированных вызовов".
Почему и на входе и на выходе? Без Непрямого Эффекта Инварианта достаточно было бы проверки на выходе, при условии проверки процедур создания. Но теперь мы должны быть более аккуратными, поскольку между завершением одного вызова и началом вызова другой операции над тем же объектом, могут быть вызовы, задевающие объект, даже если в роли цели выступал совсем другой объект.
Более удовлетворительное решение могло быть получено включением статистического правила, имеющего обязательную силу, гарантирующего, что всякий раз, когда инвариант класса А включает ссылки на экземпляры класса В, инвариант в классе В должен быть зеркальным отображением инварианта из А. В нашем примере можно избежать всех трудностей, включив в класс В инвариант:
trip_round: (backward /= Void) implies (backward.forward = Current)
Быть может, возможно, обобщить это правило в универсальное правило отображения. Вне зависимости от того, существует ли такое обещающее правило или нет, решение проблемы Непрямого Эффекта Инварианта и избавление необходимости двойной проверки при мониторинге инвариантов требует дальнейших исследований.
Что дальше
Еще не все сделано с Проектированием по контракту. Предстоит изучить два важных следствия рассмотренных принципов:
[x]. Как они приводят к механизму дисциплинированной обработки исключений; это тема следующей лекции.
[x]. Как они комбинируются с наследованием, позволяя нам указать, что любые семантические ограничения, применимые к классу, применимы также и к его потомкам; и что семантические ограничения, применимые к компоненту, применимы и при возможных его переопределениях. Эта тема будет изучаться при рассмотрении наследования.
Обобщая, утверждения и Проектирование по контракту будут сопровождать нас во всей оставшейся части этой книги, позволяя проверить, знаем ли мы, что делают создаваемые нами элементы.
Ключевые концепции
[x]. Утверждения - это булевы выражения, задающие семантические свойства класса и вводящие аксиомы и предусловия соответствующего абстрактного типа данных.
[x]. Утверждения используются в предусловиях (требования, при выполнении которых программы применимы), постусловиях (свойства, гарантируемые на выходе программ), и инвариантах класса (свойства, характеризующие экземпляры класса во время их жизни). Другими конструкциями, включающими утверждения, являются инварианты цикла и инструкции check.
[x]. Предусловие и постусловие программы описывают контракт между программой и ее клиентами. Контракт связывает программу, только при условии ее вызова, в состоянии, где предусловие выполняется; в этом случае программа гарантирует выполнимость постусловия на выходе. Понятие заключения контрактов между программами обеспечивает мощную метафору при построении надежного ПО.
[x]. Инвариант класса выражает семантические ограничения экземпляров класса. Инвариант неявно добавляется к предусловиям и постусловиям каждой экспортируемой программы класса.
[x]. Класс описывает одну возможную реализацию АТД; отображение класса в АТД выражается функцией абстракции, обычно частичной. Обратное отношение, обычно, не задается функцией.
[x]. Инвариант реализации, - часть инварианта класса - выражает корректность представления классом соответствующего АТД.
[x]. Цикл может иметь инвариант цикла, позволяющий вывести результат выполнения цикла, и вариант, позволяющий доказать завершаемость цикла.
[x]. Если класс поставляется с утверждениями, то можно формально определить, что означает корректность класса.
[x]. Утверждения служат четырем целям: помогают в конструировании корректных программ; помогают в создании документации, помогают в отладке, являются основой механизма исключений.
[x]. Язык утверждений в нашей нотации не включает логику предикатов первого порядка, но может выражать многие свойства высокого уровня благодаря вызову функций. Функции, включаемые в утверждения должны быть простыми и безупречно корректными.
[x]. Комбинация инвариантов и динамических псевдонимов приводит к Непрямому Эффекту Инварианта, который может стать причиной нарушения инварианта при корректности самого класса.
