Основы объектно-ориентированного программирования - Бертран Мейер
Шрифт:
Интервал:
Закладка:
-- Создать массив с границами 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) - визави соответствующего АТД.
