Бертран Мейер - Основы объектно-ориентированного программирования
[x]. Функция new создает пустой стек.
В разделе ФУНКЦИИ эти функции определяются не полностью, вводятся только их сигнатуры - списки типов их аргументов и результата. Сигнатура функции put
STACK [G] × G STACK [G]
показывает, что put берет в качестве аргумента пару вида <s,x>, в которой s - экземпляр типа STACK [G], а x - экземпляр типа G, и возвращает в качестве результата экземпляр типа STACK [G]. Вообще говоря, множество значений функции (его тип указывается в сигнатуре правее стрелки, здесь это STACK [G]) может само быть декартовым произведением. Это можно использовать при описании операций, возвращающих два или более результатов.
В сигнатуре функций remove и item вместо обычной стрелки используется перечеркнутая стрелка . Это означает, что эти функции применимы не ко всем элементам множества входов. Описание функции new выглядит просто как
new: STACK
без всякой стрелки в сигнатуре. Фактически, это сокращение для записи
new: STACK,
определяющей функцию без аргументов. Здесь аргументы не нужны, поскольку new должна всегда возвращать один и тот же результат - пустой стек. Поэтому для простоты мы убрали здесь стрелку. Результат применения этой функции (т. е. пустой стек) будет записываться new, как сокращение для new(), обозначающего результат применения new к пустому списку аргументов.
Категории функций
В начале этой лекции операции над типами были разделены на конструкторы, запросы и команды. В спецификации АТД для нового типа T, например для STACK [G] в нашем примере можно определить эту классификацию более строго. Эта классификация просто проверяет, где по отношению к стрелке расположен в сигнатуре каждой функции тип T:
В альтернативной терминологии эти три категории называются "конструктор", "аксессор" и "модификатор". Здесь мы придерживаемся терминов, более непосредственно связанных с интерпретацией функций АТД как моделей операций над программными объектами.[x]. Функция, в сигнатуре которой T появляется лишь справа от стрелки, например new, является функцией-конструктором. Она моделирует операцию, создающую экземпляры T из экземпляров других типов или вообще не использующую аргументов, например как в случае константного конструктора new.
[x]. Такие функции как item и empty, у которых T появляется только слева от стрелки, являются функциями-запросами. Они моделируют операции, которые устанавливают свойства T, выраженные в терминах экземпляров других типов (в наших примерах - это BOOLEAN и параметр типа G).
[x]. Такие функции как put и remove, у которых T появляется с обеих сторон стрелки, являются функциями-командами. Они моделируют операции, которые по существующим экземплярам T и, возможно, экземплярам других типов выдают новые экземпляры типа T.
Раздел АКСИОМЫ
Мы уже видели, как типы данных (например, 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 он выглядит следующим образом.
Аксиомы
Для всех x: G, s: STACK [G],
[x]. (A1) item (put (s, x)) = x
[x]. (A2) remove (put (s, x)) = s
[x]. (A3) empty (new)
[x]. (A4) not empty (put (s, x))
Первые две аксиомы выражают основные свойства стеков (последним пришел - первым ушел) LIFO. Чтобы понять их, предположим, что у нас есть стек s и экземпляр x, и определим s' как результат put(s, x) , т. е. как результат вталкивания x в s. Приспособим один из предыдущих рисунков:
Рис. 6.4. Применение функции put
Здесь аксиома A1, говорит о том, что вершиной s' является x - последний элемент, который мы втолкнули, а аксиома A2 объясняет, что при удалении верхнего элемента s' мы снова получаем тот же стек s, который был до вталкивания x. Эти две аксиомы дают лаконичное описание главного свойства стеков в чисто математических терминах без всякой помощи императивных рассуждений или ссылок на свойства представлений.
Аксиомы A3 и A4 говорят о том, когда стек пуст, а когда - нет: стек, полученный в результате работы конструктора new пустой, а всякий стек, полученный после вталкивания элемента в уже существующий стек (пустой или непустой) не является пустым.
Эти аксиомы, как и остальные, являются предикатами (в смысле логики), выражающими истинность некоторых свойств для всех возможных значений s и x. Некоторые предпочитают рассматривать A3 и A4 в другой эквивалентной форме как определение функции empty индукцией по размеру стеков:
Для всех x: G, s: STACK [G]
A3' · empty (new) = true
A4' · empty (put (s, x)) = false
Две или три вещи, которые мы знаем о стеках
Спецификации АТД являются неявными. Имеются два вида "неявности":
[x]. Метод АТД определяет неявно некоторое множество объектов, задавая применимые к ним функции. Из этого определения никогда не следует, что в нем перечислены все операции; часто, на пути к представлению, будут добавлены и другие.
[x]. Сами функции также определяются неявно. Вместо явных определений используются аксиомы, задающие свойства этих функций. Здесь тоже ничего не утверждается о полноте: когда вы, в конце концов, дойдете до реализации этих функций, они приобретут дополнительные свойства.
