Кажется, совместно эти два условия гарантируют, что INV действительно инвариант. Доказательство почти тривиально: так как INV удовлетворяется в момент создания и сохраняется при каждом вызове, то по индукции INV истинно во все стабильные времена.
Это неформальное доказательство, однако, не верно в присутствии семантики ссылок и динамических псевдонимов. Проблема в том, что атрибуты объекта могут модифицироваться операциями другого объекта. Даже если a.r сохраняет INV для объекта ОА, присоединенного к а, то некоторая операция b.s (для b, присоединенного к другому объекту,) может разрушить INV для ОА. Так что условия (1) и (2) могут выполняться, но INV может не быть инвариантом.
Вот простой пример. Предположим, что А и В классы, каждый из которых содержит атрибут другого класса:
class A ... feature forward: B ... end
class B ... feature backward: A ... end
Потребуем, чтобы ссылки были связаны содержательным условием. Если ссылка 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 далеко не академический пример, это, как отмечалось, полезный образец для практических приложений и библиотек.
