Функциональная спецификация стека

Стек (st ac k) — это специальный тип списка, в котором все вставки и удаления элементов выполняются только на одном конце, называемом вершиной (top). Такой метод доступа обозначается аббревиатурой LIFO (last-in-first-out — последним пришел — первым вышел).

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

1. Создание пустого стека — операция Create;

2. Проверка стека на наличие в нем хотя бы одного элемента — предикат (логическая функция) IsNull.

3. Получение элемента из вершины непустого стека — операция GetTop;

4. Удаление элемента с вершины непустого стека (элемент выталкивается из стека) — операция Pop;

5. Вставка значения х в вершину стека (элемент заталкивается в стек) — операция Push.

Операция Сreate представляет собой примитивный конструктор, операция IsNull — индикатор, GetTop — селектор, операции Push и Pop — модификаторы.

Хотя семантика этих операций интуитивно понятна из их неформального описания, перед тем, как начать реализацию, рассмотрим формальную спецификацию каждой операции, применив алгебраический подход [2].

Спецификацию каждой операции представим в виде:

операция: множество входных данных ® множество выходных данных

Множество входных или выходных данных задается с помощью указания их типа, при этом, если операция имеет несколько аргументов или результатов, при задании спецификации будет использоваться символ Ä, обозначающий декартово произведение множеств.

Пусть стек состоит изэлементов типа α. Введем новый типданных Stack of αº Stack (α). Непустой стек обозначим как Non _ null _ stack.

Базовый набор операций определяется так:

1. Create:  ® Stack (α);

2. IsNull: Stack (α) ® Boolean;

3. GetTop: Non_null_stack (α) ® α;

4. Pop: Non_null_stack (α) ® Stack (α);

5. Push: α Ä Stack (α) ® Stack (α)

Дополним данное определение набором аксиом, которые справедливы для вышеуказанных операций. Пусть p — значение типа α; s —stack (α):

A1. IsNull (Create) = true;

A2. IsNull (Push (p, s)) = false;

A3. GetTop (Push (p, s)) = p;

A4. Pop (Push (p, s)) = s;

A5. Push (GetTop (s), Pop (s)) = s.

Часто при определении стека вместо операции Pop используют операцию, совмещающую результат действия GetTop и Pop. Обозначим такую операцию Pop 2. Тогда

Pop2: Non_null_stack (α) ® α Ä Stack (α).

Функциональная спецификация очереди

Очередь(queue) - это другой специальный тип списка, где элементы вставляются в конец списка, называемый хвостом (tail), а удаляются из начала списка, называемого головой (head). Очереди также называют "списками типа FIFO" (аббревиатура FIFO расшифровывается как first-in-first-out: первым вошел — первым вышел). Операции, выполняемые с очередями, аналогичны операциям со стеками.

К сожалению, для обозначения операций нет стандартных устоявшихся названий. Воспользуемся обозначениями, которые предлагаются в книгах Ахо и Седжвика.

1. Создание пустой очереди — операция create

2. Проверка очереди на наличие хотя бы одного элемента — предикат (логическая функция) isnull.

3. Вставка значения p в конец (хвост) очереди — операция enqueue;

4. Удаление элемента из начала (головы) непустой очереди с получением его значения — операция dequeue. Эту операцию можно рассматривать и как две различные операции: head — получение первого элемента из головы очереди и собственно dequeue — удаление элемента.

Формальная спецификация операций для очереди из элементов типа α (Queue of αº Queue (α)) [2] выполняется аналогично спецификации стека.

1. Create: ® Null_queue (α);

2. IsNull: Queue (α) ® Boolean;

3. EnQueue: Queue (α) Ä α ® Queue (α);

4. GetHead: Non_null_queue (α) ® α;

5. DeQueue: Non_null_queue (α) ® Queue (α).

Приведем набор аксиом, справедливых для данных операций. Пусть p — значение типа α; q —queue (α):

A1. IsNull (Create) = true;

A2. IsNull (EnQueue (q, p)) = false;

A3. GetHead (EnQueue (q, p)) =

если IsNull (q) то p иначе Head (q);

A4. DeQueue (EnQueue (q, p)) =

если IsNull(q) то Create иначе EnQueue(DeQueue(q),p).

Деки

Иногда используют списки, в которых вставка и удаление элементов выполняются с обоих концов. Такой список называется деком. (сокращение от английского double ended queue- о чередь с двумя концами).

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

Формальную спецификацию дека можно выполнить аналогично стеку или очереди.