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

[x]. Сами функции также определяются неявно. Вместо явных определений используются аксиомы, задающие свойства этих функций. Здесь тоже ничего не утверждается о полноте: когда вы, в конце концов, дойдете до реализации этих функций, они приобретут дополнительные свойства.

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

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

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

Частичные функции

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

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

inv(x)= 1/x.

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

Inv: R R

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

Областью (определения) частичной функции типа X Y является подмножество тех элементов X, для которых эта функция имеет некоторое значение. В нашем примере областью функции inv является R - {0}, т.е. множество действительных чисел, отличных от 0.

В спецификации АТД STACK эти идеи использованы для стеков при объявлении remove и item как частичных функций в разделе ФУНКЦИИ - это указано с помощью перечеркнутых стрелок в их сигнатуре. При этом возникает новая проблема, обсуждаемая в следующем пункте: как задавать области таких функций?

В некоторых случаях функцию put тоже желательно описывать как частичную, например, это требуется в таких реализациях как МАССИВ_ВВЕРХ и МАССИВ_ВНИЗ, которые поддерживают выполнение лишь конечного числа подряд идущих операций put для каждого заданного стека. Это на самом деле полезное упражнение - приспособить спецификацию STACK к тому, чтобы она описывала ограниченные стеки конечного объема, поскольку в приведенном выше виде она не содержит никаких ограничений на размеры стеков.

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

Предусловия

Частичные функции являются неустранимым фактом процесса проектирования ПО, отражающим очевидное наблюдение: не каждая операция применима ко всем объектам. Но они также являются и потенциальным источником ошибок: если функция 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), так что предусловие может ссылаться на эти аргументы.

BOOLEAN такая, что ch(x) истинна, если x принадлежит A, и ложна в противном случае.

Полная спецификация

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

Спецификация стеков как АТД

ТИПЫ (TYPES)

[x]. STACK [G]

ФУНКЦИИ (FUNCTIONS)

[x]. put: STACK [G] × G STACK [G]

[x]. remove: STACK [G] STACK [G]

[x]. item: STACK [G] G

[x]. empty: STACK [G] BOOLEAN

[x]. new: STACK [G]

АКСИОМЫ (AXIOMS)

Для всех 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))

ПРЕДУСЛОВИЯ (PRECONDITIONS)

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

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

Ничего кроме правды

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

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

Вот пример. Рассмотрим для приведенной выше спецификации АТД STACK следующее выражение stackexp:

item (remove (put (remove (put (put (

remove (put (put (put (new, x1), x2), x3)),

item (remove (put (put (new, x4), x5)))), x6)), x7)))

По-видимому, выражение stackexp будет проще понять, если мы представим его как последовательность вспомогательных выражений:

s1 = new

s2 = put (put (put (s1, x1), x2), x3)

s3 = remove (s2)

s4 = new

s5 = put (put (s4, x4), x5)

s6 = remove (s5)

y1 = item (s6)

s7 = put (s3, y1)

s8 = put (s7, x6)

s9 = remove (s8)

s10 = put (s9, x7)

s11 = remove (s10)

stackexp = item (s11)

Какой бы вариант определения вы ни выбрали, по нему несложно восстановить вычисление, математической моделью которого является stackexp: создать новый стек; втолкнуть в него элементы x1, x2, x3 (в указанном порядке); удалить верхний элемент (x3), назвав получившийся стек s3; создать другой пустой стек и т. д. Этот процесс графически представлен на рис. 6.5.