Бертран Мейер - Основы объектно-ориентированного программирования

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

Это неформальное требование достаточно ясно на практике; формализм подъязыка 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 .

Кажется, совместно эти два условия гарантируют, что INV действительно инвариант. Доказательство почти тривиально: так как INV удовлетворяется в момент создания и сохраняется при каждом вызове, то по индукции INV истинно во все стабильные времена.

Это неформальное доказательство, однако, не верно в присутствии семантики ссылок и динамических псевдонимов. Проблема в том, что атрибуты объекта могут модифицироваться операциями другого объекта. Даже если a.r сохраняет INV для объекта ОА, присоединенного к а , то некоторая операция b.s (для b , присоединенного к другому объекту,) может разрушить INV для ОА. Так что условия (1) и (2) могут выполняться, но INV может не быть инвариантом.

Вот простой пример. Предположим, что А и В классы, каждый из которых содержит атрибут другого класса: