помеченные на рисунке штрихованными линиями, ведут к одному и тому же значению - абстрактному объекту
[x]. Применить конкретную функцию класса
[x]. Применить функцию абстракции
Инварианты реализации
Некоторые утверждения появляются в реализации, хотя они не имеют прямых двойников в спецификации АТД. Эти утверждения используют атрибуты, включая некоторые закрытые атрибуты, которые, по определению, не имеют смысла в АТД. Простым примером являются свойства, появляющиеся в инварианте
count_non_negative: 0 <= count
count_bounded: count <= capacity
Такие утверждения составляют часть инварианта класса, известную как инвариант реализации (implementation invariant). Они позволяют задать соответствие представления реализации, выбранное в классе, (здесь это атрибуты
Рис. 11.5 помогает понять концепцию инварианта реализации. Он иллюстрирует характеристические свойства функции абстракции, представленной вертикальной стрелкой на рисунке. Об этом стоит поговорить подробнее.
Прежде всего, корректно ли рассматривать
Так как интерфейс класса ограничен компонентами, непосредственно выводимыми из функций АТД, клиенты не имеют способа различать поведение конкретных объектов, представляющих один и тот же абстрактный стек (это и есть причина, по которой все они имеют одну функцию абстракции
count := count - 1
не пытаясь очистить выше расположенные элементы. Всякое изменение элементов, расположенных выше
Итак, отношение реализации это обычно не функция. Но инверсия этого отношения - функция абстракции - действительно является функцией, так как каждому конкретному объекту ставится в соответствие один абстрактный объект. В примере стека каждой правильной паре
Рис. 11.6. Один абстрактный объект и два его представления
Оба конкретных стека, изображенные на рисунке, являются реализациями абстрактного стека, состоящего из трех элементов со значениями: 342, -133, 5. Отображение
Функция абстракции
В математических терминах, инвариант реализации является характеристической функцией области определения абстрактной функции. Другими словами, это булево свойство, определяющее применимость функции. (Характеристическая функция подмножества
Инвариант реализации является той частью утверждений класса, у которой нет двойника в спецификации АТД. Он не связан с АТД, и относится только к реализации. Он определяет, при каких условиях кандидат - конкретный объект - действительно является реализацией одного и только одного абстрактного объекта.
Инструкция утверждения
Утверждения, рассматриваемые до сих пор - предусловия, постусловия, инварианты, - это основные составляющие метода. Они устанавливают связь между конструкциями ОО-программных систем и теорией АТД, лежащей в основе метода. Инварианты класса, в частности, не могут быть поняты, и даже обсуждаться вне рамок ОО-подхода.
Можно рассматривать и другие возможности использования утверждений. Хотя они менее специфичны для нашего метода, но тоже играют важную роль, и должны быть частью нашей нотации.
