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

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

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

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

Инварианты класса и семантика ссылок

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

[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

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)

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

Date: 2015-12-13; view: 439; Нарушение авторских прав