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

class STACK4 [G] creation

...Как в STACK2...

feature

...Как в STACK2...

invariant

count_non_negative: 0 <= count

count_bounded: count <= capacity

consistent_with_array_size: capacity = representation.capacity

empty_if_no_elements: empty = (count = 0)

item_at_top: (count > 0) implies (representation.item (count) = item)

end

Инвариант класса C это множество утверждений, которым удовлетворяет каждый экземпляр класса во все "стабильные" времена. В эти времена экземпляр класса находится в наблюдаемом состоянии:

[x].на момент создания экземпляра, сразу после выполнения create aили create a.make(...), где a класса C ;

[x].перед и после каждого удаленного вызова a.r(...) программы r класса С .

Следующий рисунок, показывающий жизнь объектов, поможет разобраться в инвариантах и стабильных временах:

Рис. 11.4. Жизнь объектов

Жизнь объектов не столь уж захватывающая. Вначале - слева на рисунке - он просто не существует. При выполнении инструкции create a или create a.make(...) или clone объект создается и достигает первой станции S1 в своей жизни. Затем идет череда довольно скучных событий: клиенты, для которых доступен объект, один за другим вызывают его компоненты в форме a.f(..) . Так все продолжается, пока не завершится вычисление.

Инвариант является характеристическим свойством состояний, представленных большими квадратиками на рисунке: S1, S2, S3 и т.д. Эти состояния соответствуют стабильным временам, упомянутым выше.

Несмотря на свое имя, инвариант не должен выполняться во все времена. Вполне законно, что некоторая процедура g , начиная выполнять свою работу, разрушает инвариант, а, завершая работу, восстанавливает его истинность. В промежуточном состоянии, показанном на рисунке маленьким квадратиком, инвариант не выполняется, но инвариант всегда должен выполняться в заключительном состоянии каждой процедуры. И в человеческом сообществе многие, стараясь сделать что-либо полезное, начинают с того, что разрушают существующий порядок вещей.

Квалифицированные вызовы в форме a.f(...) , выполняемые на стороне клиента, всегда начинаются и заканчиваются в состоянии, удовлетворяющем инварианту. Подобного правила нет для неквалифицированных вызовов в форме f(...) , недоступных для клиентов, но используемых в квалифицированных вызовах для служебных целей. Как следствие, обязанность управлять инвариантами возлагается только на модули, экспортируемые всем клиентам или выборочно. Закрытые методы, недоступные клиентам, не обязаны беспокоиться об инвариантах.

Закончим обсуждение правилом, точно определяющим, когда утверждение является корректным инвариантом класса:

Правило инварианта

Утверждение Inv является корректным инвариантом класса, если и только если оно удовлетворяет следующим двум условиям:

1Каждая процедура создания, применимая к аргументам, удовлетворяющим ее предусловию в состоянии, в котором атрибуты имеют значения, установленные по умолчанию, вырабатывает заключительное состояние, гарантирующее выполнение Inv .

2Каждая экспортируемая процедура класса, примененная к аргументам в состоянии, удовлетворяющем Inv и предусловию, вырабатывает заключительное состояние, гарантирующее выполнение Inv .

Заметьте, в этом правиле:

[x].Предполагается, что каждый класс обладает процедурой создания, задаваемой конструктором по умолчанию, при отсутствии явного ее определения.

[x].Состояние объекта определяется значениями всех его полей (значениями атрибутов класса для этого конкретного экземпляра).

[x].Предусловие программы может включать начальное состояние и аргументы.

[x].Постусловие может включать только заключительное состояние, начальное состояние, (используя нотацию old) и, в случае функций, возвращаемое значение, заданное предопределенной сущностью Result .