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

         

Форма и свойства инвариантов класса


Синтаксически инвариант класса является утверждением, появляющимся в предложении invariant, стоящим после всех предложений feature, и перед предложением end. Вот пример:

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 это множество утверждений, которым удовлетворяет каждый экземпляр класса во все "стабильные" времена. В эти времена экземпляр класса находится в наблюдаемом состоянии:

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

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


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

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

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

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



Содержание раздела