Абстрактный тип данных

Языки алгебраических спецификаций

В предыдущем разделе мы рассмотрели основы математической теории многосортных алгебраических систем. Было показано, что абстрактные типы данных также описываются этой теорией. Абстрактный тип данных представляется сигнатурой Σ-алгебры, содержащей имена сортов и операций. Также, абстрактный тип данных снабжается конечным набором аксиом-равенств, выражающих закономерности, присущие данному типу данных.
В классе всех Σ-алгебр сигнатуры Σ=(S,OP) имеется т.н. инициальная алгебра, из которой имеется единственный гомоморфизм в каждую Σ-алгебру данного класса. Инициальная алгебра строится синтаксически как множество термов, составленных из констант сигнатуры Σ, и имен операций этой сигнатуры.
Инициальная алгебра позволяет производить проверку корректности спецификации АТД, а также проверять спецификацию на наличие ошибок другого рода. Следует отметить, что подобным способом (в виде сигнатур Σ-алгебр) можно описывать не только абстрактные типы данных. Сигнатуры с аксиомами в виде равенств можно использовать для различного рода описаний. Такие описания, выполненные в виде сигнатур, называются алгебраическими спецификациями.
За прошедшие три с лишним десятка лет было придумано множество языков алгебраических спецификаций. Одним из первых языков такого рода был OBJ [12], реализованный Джозефом Гогеном в середине 70-х годов прошлого века. Вот как выглядит спецификация конечного автомата на этом языке.

th AUTOMATON issorts Input State Output . op s0 : -> State . op f : Input State -> State . op g : State -> Output . endth

Абстрактный тип данных «конечный автомат» вводится с помощью ключевого слова «th» или «theory». Затем идет спецификация сортов и операций. Поясним их смысл.
Конечный автомат неформально можно представить как конечное множество состояний и функцию переходов, которая берет на вход пару (символ, состояние) и возвращает состояние в качестве результата. В конечном автомате выделяются начальное состояние и множество допускающих состояний. В начале работы конечный автомат устанавливается в начальное состояние, после чего по входной последовательности символов производятся переходы.
В данной выше спецификации конечного автомата задается три сорта. Сорт Input представляет множество символов, которые подаются на вход автомату. Сорт State представляет множество состояний, а сорт Output представляет множество символов, которые выдаются на печать для каждого состояния. Описываемый тип конечного автомата, который печатает значения для каждого состояния, называется трансдьюсером. Для трансдьюсеров допускающие состояния не столь важны, поэтому здесь они не заданы.
Операция s0 – это константа, задающая начальное состояние. Двухместная операция f представляет функцию переходов автомата. Операция g описывает функцию вывода трансдьюсера.
Одним из наиболее популярных на данный момент языков алгебраических спецификаций является CASL [13]. Язык CASL является результатом разработки инициативной группы CoFI (Common Framework Initiative for algebraic specification and development of software) [14], организованной в 1995 году специально для создания языка алгебраических спецификаций.
Приведу пример спецификации моноида на языке CASL. Моноид – это алгебраическая структура, с одной операцией, которая удовлетворяет свойству ассоциативности. Также в моноиде имеется нейтральный элемент, который при взаимодействии с другими элементами оставляет их без изменений. Примером моноида является множество натуральных чисел, включающее нуль, который играет роль нейтрального элемента относительно операции сложения натуральных чисел. Итак, приведем пример спецификации.

spec Monoid = sort Elem ops n : Elem; __*__ : Elem x Elem -> Elem; forall x,y,z : Elem * n*x=x * x*n=x * (x*y)*z=x*(y*z)

Как видно, определяет спецификация типа Monoid, в котором имеется один сорт с именем Elem и две операции: константа n и «*». Также задаются три аксиомы-равенства. Первые две аксиомы описывают взаимодействие с нейтральным элементом, а третья аксиома – ассоциативность операции «*».