Бертран Мейер - Основы объектно-ориентированного программирования

Это определение функции 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].Сами функции также определяются неявно. Вместо явных определений используются аксиомы, задающие свойства этих функций. Здесь тоже ничего не утверждается о полноте: когда вы, в конце концов, дойдете до реализации этих функций, они приобретут дополнительные свойства.

Эта неявность является ключевым аспектом абстрактных типов данных и, как следствие, - их будущих аналогов в построении ОО-ПО - классов. Когда мы определяем абстрактный тип данных или класс, мы всегда сообщаем кое-что об этом типе или классе, просто перечисляя те их свойства, которые знаем, и берем их в качестве определения. При этом никогда не предполагается, что других применимых свойств нет.

Неявность также предполагает открытость определений: всегда можно добавить новые свойства АТД или класса. Основным механизмом для выполнения таких расширений без разрушения уже существующего первоначального определения является наследование.

Этот "неявный" подход имеет далеко идущие последствия. В пункте "дополнительные темы" в конце этой лекции помещены еще некоторые комментарии о неявности.

Спецификация всякого реалистичного примера, даже такого простого как стеки, неизбежно сталкивается с проблемами не всюду определенных операций: некоторые операции применимы не ко всем возможным элементам исходных множеств. Например, это имеет место для функций remove и item : нельзя удалить элемент из пустого стека, и у пустого стека нет верхнего элемента.

Решение этой проблемы, использованное в приведенной выше спецификации, состоит в том, чтобы определить эти функции как частичные. Функция из исходного множества X в результирующее множество Y является частичной, если она определена не для всех элементов X . Функция, не являющаяся частичной, называется полной. Простым примером частичной функции в обычной математике является функция обращения действительных чисел inv , значение которой на действительном числе x равно

inv(x)= 1/x.

Поскольку inv не определена при x = 0 , мы можем определить ее как частичную функцию на множестве R всех действительных чисел:

Inv: R R

Чтобы указать, что функция частичная, используется перечеркнутая стрелка будет означать, что функция заведомо полная.

Областью(определения) частичной функции типа X

Предусловия

Частичные функции являются неустранимым фактом процесса проектирования ПО, отражающим очевидное наблюдение: не каждая операция применима ко всем объектам. Но они также являются и потенциальным источником ошибок: если функция f из X в Y является частичной, то нельзя быть уверенным в том, что выражение f(e) имеет смысл, даже если e принадлежит X - требуется гарантировать, что это значение принадлежит области f .

Для этого всякая спецификация АТД, содержащая частичные функции, должна задавать их области. В этом и состоит роль раздела ПРЕДУСЛОВИЯ (PRECONDITIONS). Для АТД STACK этот раздел выглядит так:

Предусловия (preconditions)

[x]. remove (s: STACK [G]) require not empty (s)

[x]. item (s: STACK [G]) require not empty (s)

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

Булевское выражение, которое определяет область функции, называется предусловиемсоответствующей частичной функции. В нашем случае предусловия обеих функций remove и item утверждают, что стек должен быть непустым. Перед "требует" помещается имя функции с именами ее аргументов (в примере для аргумента-стека использовано s ), так что предусловие может ссылаться на эти аргументы.