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

В некоторых случаях функцию 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, и ложна в противном случае.

С точки зрения математики предусловие функции f - это характеристическая функция области f. Характеристической функцией подмножества Aмножества X называется полная функция ch: X

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

Раздел ПРЕДУСЛОВИЯ (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)))