Инварианты класса и семантика ссылок
ОО-модель, разрабатываемая до сих пор, включала два частично не связанных аспекта, оба из которых полезны:
[x]. Понятие инварианта класса, введенное в этой лекции.
[x]. Гибкая модель периода выполнения, детально рассмотренная в начальных лекциях, существенно использующая ссылки.
К несчастью, эти индивидуально желательные свойства могут стать причиной трудностей при их совместном использовании.
Проблема вновь в динамически создаваемых псевдонимах, предохраняющих нас от проверки корректности класса на том основании, что класс делает это сам. Мы уже видели, что корректность класса означает проверку m+n свойств, выражающих следующее (если мы концентрируем внимание на инвариантах INV, игнорируя предусловия и постусловия, не играющие здесь роли):
1 Каждая из m процедур создания порождает объект, удовлетворяющий INV.
2 Каждая из n экспортируемых программ сохраняет INV.
Кажется, совместно эти два условия гарантируют, что 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
