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

-- Создать массив с границами minindex и maxindex

-- (пустой если minindex > maxindex).

require

meaningful_bounds: maxindex >= minindex - 1

do

...

ensure

exact_bounds_if_non_empty: (maxindex >= minindex) implies

((lower = minindex) and (upper = maxindex))

conventions_if_empty: (maxindex < minindex) implies

((lower = 1) and (upper = 0))

end

feature -- Access (Доступ)

lower, upper, count: INTEGER

-- Минимальное и максимальное значение индекса; размер массива.

infix "@", item (i: INTEGER): G is

-- Элемент с индексом i

require

index_not_too_small: lower <= i

index_not_too_large: i <= upper

do ... end

feature -- Element change (Изменение элементов)

put (v: G; i: INTEGER) is

-- Присвоить v элементу с индексом i

require

index_not_too_small: lower <= i

index_not_too_large: i <= upper

do

...

ensure

element_replaced: item (i) = v

end

invariant

consistent_count: count = upper - lower + 1

non_negative_count: count >= 0

end

Единственное, что не конкретизировано в описании этого класса, это реализация программ item и put. Поскольку эффективная манипуляция с массивом требует доступа к системам низкого уровня, то эти программы будут реализованы с использованием внешних классов, что будет рассмотрено в последующих лекциях.

Связывание с АТД

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

Не просто коллекция функций

Как отмечалось в лекции про АТД, они включают четыре элемента:

[x]. имя типа, возможно с родовым параметром (раздел TYPES);

[x]. список функций с их сигнатурами (раздел FUNCTIONS);

[x]. аксиомы, выражающие свойства результатов функций (раздел AXIOMS);

[x]. ограничения применимости функций (раздел PRECONDITIONS).

При поверхностном применении АТД часто опускают две последние части. Во многом, это лишает данный подход привлекательности, поскольку предусловия и аксиомы выражают семантические свойства функций. Если их опустить и просто рассматривать стек как инкапсуляцию операций put, remove и других, то преимущества от скрытия информации останутся, но это все. Понятие стека становится пустой оболочкой без семантики, кроме той, что остается в именах функций. (В этой книге имена функций менее информативны по причине согласованности и повторного использования, - мы сознательно выбрали общие имена - put, remove, item, а не те, которые применяются обычно для стеков - push, pop, top).

Этот риск потери семантики переносится на программирование: программы, реализующие операции соответствующего АТД, в принципе могут выполнять нечто отличное от задуманного. Утверждения предотвращают этот риск, возвращая семантику классу.

Компоненты класса и АТД функции

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

f : A × B × ... X

зависит от того, где имя АТД, скажем T, встречается среди типов A, B, ... X, включенных в эту сигнатуру:

[x]. Если Т появляется только справа от стрелки, f является создателем; в классе это соответствует процедуре создания.

[x]. Если Т появляется только слева от стрелки, f является запросом, обеспечивающим доступ к свойству экземпляра класса. Для класса запрос соответствует атрибуту или функции; термин запрос сохраняется и для класса, когда нет необходимости различать, как он реализован.

[x]. Если Т появляется как слева, так и справа от стрелки, f является командой, вырабатывающей новый объект из одного или нескольких уже существующих. На этапе реализации f часто задается процедурой (также называемой командой), которая модифицирует существующий объект, не создавая новый, как это делают функции.

Выражение аксиом

Из соответствия между АТД функциями и компонентами класса можно вывести соответствие между утверждениями класса и семантическими свойствами АТД.

[x]. Предусловие для специфицированной в АТД функции появляется как предусловие программы, соответствующей данной функции.

[x]. Аксиома, включающая команду, и, возможно, одну или более функций запросов, появится как постусловие соответствующей процедуры.

[x]. Аксиомы, включающие только запросы, появятся как постусловия соответствующих функций или как инвариант. Последнее обычно имеет место, если более чем одна функция включена в аксиому, или, по меньшей мере, один из запросов реализован в виде атрибута.

[x]. Аксиомы, включающие функцию создатель, появятся в постусловии соответствующей процедуры создания.

В этот момент следует вернуться назад и сравнить аксиомы АТД STACK с утверждениями класса STACK4 (включая и те, которые даны для класса STACK2).

Функция абстракции

Этот раздел требует от читателя определенной математической подготовки.

Полезно рассмотреть предшествующее обсуждение в терминах следующего рисунка, навеянного работой [Hoare 1972a], в которой описывается понятие "С является корректной реализацией А".

Рис. 11.5.  Преобразования между абстрактными и конкретными объектами

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

Стрелка, помеченная а, представляет функцию абстракции (abstraction function), которая для любого экземпляра класса - конкретного объекта - возвращает соответствующий абстрактный объект (экземпляр АТД). Как будет видно, функция обычно бывает частичной, а обратное отношение обычно не является функцией.

Реализация корректна, если (для всех функций af из АТД и их реализаций cf) диаграмма коммутативна, или, как говорят, имеет место:

Свойство согласованности Класс-АТД

(cf;a) = (a;af)

где символ ";" обозначает композицию функций. Другими словами, для любых двух функций f и g, их композиция: f;g задает функцию h, такую что h(x) = g(f(x)) для каждого применимого x.

(Композицию f;g также записывают в виде: g ° f, с обратным порядком применения операндов.)

Свойство устанавливает, что для каждого конкретного объекта CONC_1 не имеет значения, в каком порядке применяются преобразования (функция абстракции, а затем af или вначале cf, а потом функция абстракции); оба пути, помеченные на рисунке штрихованными линиями, ведут к одному и тому же значению - абстрактному объекту ABST_2. Результат будет одним и тем же, если:

[x]. Применить конкретную функцию класса cf, а потом функцию абстракции а, получив a(cf(CONC_1)).

[x]. Применить функцию абстракции а, а потом функцию АТД - af, получив af(a(CONC_1)).

Инварианты реализации

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

count_non_negative: 0 <= count

count_bounded: count <= capacity

Такие утверждения составляют часть инварианта класса, известную как инвариант реализации (implementation invariant). Они позволяют задать соответствие представления реализации, выбранное в классе, (здесь это атрибуты count, capacity, representation) - визави соответствующего АТД.