Насыщенные утверждениями отложенные классы хорошо подходят для представления АТД. Прекрасный пример - отложенный класс для стеков. Мы уже описывали процедуру 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 и предусловиями процедур. Аксиомы представлены в постусловиях процедур и в инварианте класса.