[x]. Функция, в сигнатуре которой
[x]. Такие функции как
[x]. Такие функции как
Раздел АКСИОМЫ
Мы уже видели, как типы данных (например,
Чтобы указать, что речь идет о стеке, а не какой-либо другой структуре данных, имеющейся пока спецификации АТД совершенно недостаточно. Всякий распределитель, например очередь: 'первым вошел - первым вышел', также будет удовлетворять этой спецификации.
Это, конечно, не должно удивлять, поскольку в разделе
square_plus_one: R R
square_plus_one (x)= x2 + 1 (для каждого x из R)
первая строка играет роль сигнатуры, но есть еще и вторая строка, в которой определяется значение функции. Как можно достичь того же для функций АТД?
Мы не будем использовать явные определения в духе второй строки определения функции
Только чтобы убедиться в том, что мы понимаем, как может выглядеть явное определение, давайте напишем одно такое определение для приведенного ранее представления стека
put (<count, representation>, x)= <count + 1, representation [count+1: x] >
где
Это определение функции
Но это не то определение, которое бы нас устроило. 'Освободите нас от рабства представлений!' - этот лозунг Фронта Освобождения Объектов и его военного крыла (бригады АТД) является также и нашим. (Отметим, что его политическая ветвь специализируется на тяжбах: класс - действие).
Поскольку всякое явное определение заставляет выбирать некоторое представление, обратимся к неявным определениям. При этом воздержимся от определения значений функций в спецификации АТД и вместо этого опишем свойства этих значений - все их существенные свойства, но только эти свойства.
Они формулируются в разделе АКСИОМЫ (AXIOMS). Для типа STACK он выглядит следующим образом.
Аксиомы
Для всех
[x]. (A1)
[x]. (A2)
[x]. (A3)
[x]. (A4)
Первые две аксиомы выражают основные свойства стеков (последним пришел - первым ушел) LIFO. Чтобы понять их, предположим, что у нас есть стек
Рис. 6.4. Применение функции put
Здесь аксиома A1, говорит о том, что вершиной
Аксиомы A3 и A4 говорят о том, когда стек пуст, а когда - нет: стек, полученный в результате работы конструктора
Эти аксиомы, как и остальные, являются предикатами (в смысле логики), выражающими истинность некоторых свойств для всех возможных значений
Для всех x: G, s: STACK [G]
A3' · empty (new) = true
A4' · empty (put (s, x)) = false
