Раздел АКСИОМЫ

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

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

Это, конечно, не должно удивлять, поскольку в разделе ФУНКЦИИ сами функции только объявляются (так же, как в программе объявляются переменные), но полностью не определяются. В ранее рассмотренном примере математического определения:

square_plus_one: R R

square_plus_one (x)= x2 + 1 (для каждого x из R)

первая строка играет роль сигнатуры, но есть еще и вторая строка, в которой определяется значение функции. Как можно достичь того же для функций АТД?

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

Только чтобы убедиться в том, что мы понимаем, как может выглядеть явное определение, давайте напишем одно такое определение для приведенного ранее представления стека МАССИВ_ВВЕРХ. С точки зрения математики выбор этого представления означает, что экземпляр типа STACK - это пара <count, representation>, где representation - это массив, а count - это число помещенных в стек элементов. Тогда явное определение функции put (для любого экземпляра x типа G) выглядит так:

put (<count, representation>, x)= <count + 1, representation [count+1: x]>

где a [n: v] обозначает массив, полученный из a путем изменения значения элемента с индексом n на v (все остальные элементы не изменяются).

Это определение функции put является просто математической версией реализации операции put, набросок которой в стиле Паскаля приведен вслед за представлением МАССИВ_ВВЕРХ на рисунке с возможными представлениями стеков в начале этой лекции.

Но это не то определение, которое бы нас устроило. "Освободите нас от рабства представлений!" - этот лозунг Фронта Освобождения Объектов и его военного крыла (бригады АТД) является также и нашим. (Отметим, что его политическая ветвь специализируется на тяжбах: класс - действие).

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

Они формулируются в разделе АКСИОМЫ (AXIOMS). Для типа STACK он выглядит следующим образом.