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

Назад к абстрактным типам данных


Насыщенные утверждениями отложенные классы хорошо подходят для представления АТД. Прекрасный пример - отложенный класс для стеков. Мы уже описывали процедуру put, сейчас приведем возможную версию полного описания этого класса.

indexing description: "Стеки (распределительные структуры с дисциплиной Last-in, First-Out), % %не зависящие от выбора представления" deferred class STACK [G] feature -- Доступ count: INTEGER is -- Число элементов. deferred end item: G is -- Последний вставленный элемент. require not_empty: not empty deferred end feature - Отчет о статусе empty: BOOLEAN is -- Стек пустой? do Result := (count = 0) end full: BOOLEAN is -- Стек заполнен? deferred end feature - Изменение элемента put (x: G) is -- Втолкнуть x на вершину. require not full deferred ensure not_empty: not empty pushed_is_top: item = x one_more: count = old count + 1 end remove is -- Вытолкнуть верхний элемент. require not empty deferred ensure not_full: not full one_less: count = old count - 1 end change_top (x: T) is -- Заменить верхний элемент на x require not_empty: not empty do remove; put (x) ensure not_empty: not empty new_top: item = x same_number_of_items: count = old count end wipe_out is -- Удалить все элементы. deferred ensure no_more_elements: empty end invariant non_negative_count: count >= 0 empty_count: empty = (count = 0) end

Этот класс показывает, как можно реализовать эффективную процедуру, используя отложенные: например, процедура change_top реализована в виде последовательных вызовов процедур remove и put. (Такая реализация для некоторых представлений, например, для массивов, может оказаться не самой лучшей, но эффективные потомки класса STACK могут ее переопределить.)

Если сравнить класс STACK со спецификацией соответствующего АТД, приведенной в лекции 6, то обнаружится удивительное сходство. Подчеркнем, в частности, соответствие между функциями АТД и компонентами класса, и между пунктом PRECONDITIONS и предусловиями процедур. Аксиомы представлены в постусловиях процедур и в инварианте класса.


Добавление операций change_top, count и wipe_out в данном случае несущественно, так как они легко могут быть включены в спецификацию АТД (см. упражнение У6.8). Отсутствие явного эквивалента функции new из АТД также несущественно, так как созданием объектов будут заниматься процедуры-конструкторы в эффективных потомках этого класса. Остаются три существенных отличия.

Первое из них - это введение функции full, рассчитанной на реализации с ограниченным числом элементов стека, например, на реализацию массивами. Это типичный пример ограничения, которое несущественно на уровне спецификации, но необходимо для разработки практических систем. Отметим однако, что это отличие между АТД и отложенным классом можно легко устранить, включив в спецификацию АТД средства для охвата ограниченных стеков. При этом общность не будет потеряна, так как некоторые реализации (например, с помощью списков) могут реализовывать full тривиальными процедурами, всегда возвращающими ложь.

Второе отличие, отмеченное при обсуждении разработки по контракту, состоит в том, что спецификация АТД полностью аппликативна (функциональна), она включает функции без побочных эффектов. А отложенный класс, несмотря на его абстрактность, является императивным (процедурным), например put определена как процедура, изменяющая стек, а не как функция, которая берет в качестве аргумента один стек и возвращает другой.

Наконец, как тоже уже отмечалось, механизм утверждений недостаточно выразителен для некоторых аксиом АТД. Из четырех аксиом стеков

Для всех x: G, s: STACK [G],



  1. item (put (s, x)) = x



  2. remove (put (s, x)) = s



  3. empty (new)



  4. not empty (put (s, x))



все, кроме (2), имеют прямые эквиваленты среди утверждений. (Мы предполагаем, что для (3) процедуры-конструкторы у потомков обеспечат выполнение условия empty). Причины таких ограничений уже были объяснены и были намечены возможные пути их преодоления - языки формальных спецификаций IFL.


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