Переход к более императивной точке зрения

Переход к более императивной точке зрения

Переход от АТД к классам включает существенное изменение стилистики: введение изменений и императивных аргументов.

Как вы помните, спецификация абстрактных типов данных не описывает явно изменений, т. е., используя термин из теоретической информатики, является аппликативной. Все свойства АТД моделируются как математические функции, это относится к конструкторам, запросам и командам. Например, операция вталкивания для стеков моделируется функцией-командой:

put: STACK [G] ? G STACK [G],

задающей операцию, которая возвращает новый стек, а не изменяет существующий.

Классы отказываются от чисто аппликативной точки зрения на функции и переопределяют команды как операции, которые могут изменять объекты. Например, операция put будет определена как процедура, которая получает некоторый элемент типа G (формальный параметр) и модифицирует стек, вталкивая новый элемент на его вершину, не создавая нового стека.

Такое изменение стиля отражает императивные настроения, преобладающие при разработке ПО. (В качестве синонима слова "императивный" иногда используется термин "операционный"). При этом потребуется изменять аксиомы АТД. Аксиомы стеков A1 и A4, которые имели вид

[x]. (A1) item (put (s, x)) = x

[x]. (A4) not empty (put (s, x))

превратятся в императивной форме в предложение, называемое постусловием программы (routine postcondition), вводимое ключевым словом ensure (обеспечивает):

put (x: G) is

-- Втолкнуть x на вершину стека

require

... Предусловие (если таковое имеется) ...

do

... Соответствующая реализация (если известна) ...

ensure

item = x

not empty

end

Здесь постусловие объясняет, что результатом вызова программы put значение item будет равно x (втолкнутому элементу), а значение empty будет ложно.

Другие аксиомы спецификации АТД приводят к утверждению, известному как инвариант класса. Постусловия, инварианты класса и другие перевоплощения предусловий и аксиом АТД мы рассмотрим во время обсуждения утверждений и проектирования по контракту (п. 11.10 "Связь с АТД").