Роль процедур создания
Инвариант класса задает множество свойств объектов (экземпляров класса), которые должны выполняться в стабильные времена жизни объектов. В частности, эти свойства должны выполняться сразу после создания экземпляра объекта.
Стандартный механизм распределения инициализирует поля значениями по умолчанию соответствующих типов, приписанных атрибутам. Эти значения могут удовлетворять или не удовлетворять инварианту. Если нет, то требуется специальная процедура создания, инициализирующая значения атрибутов таким образом, чтобы инвариант выполнялся. Поэтому процедуру создания можно рассматривать, как операцию, гарантирующую, что все экземпляры класса начинают жить, имея корректный статус, - в котором инвариант выполняется.
При первом представлении процедур создания они рассматривались, как способ ответа на земной (и очевидный) вопрос, как переопределить инициализацию по умолчанию, если она не подходит для моего класса. Другая рассматриваемая проблема, - как задать несколько различных механизмов инициализации. Но теперь, с введением инвариантов и теоретического обсуждения, отраженного в правиле (1), мы видим более весомую роль процедур создания. Теперь они создают уверенность, что любой экземпляр класса, только начиная жить, удовлетворяет фундаментальным правилам своей касты - инварианту класса.
Ревизия массивов
Набросок библиотечного класса
Приведем улучшенный, но все еще схематичный вариант, включающий утверждения. Предусловия выражают базисные требования к доступу и модификации элементов: индексы должны быть в допустимой области. Инвариант задает отношение, существующее между
indexing
description: 'Последовательности значений одного типа или %
%согласованных типов, доступных по индексам - целым из заданного интервала %'
class ARRAY [G] creation
make
feature - Initialization (Инициализация)
make (minindex, maxindex: INTEGER) is
-- Создать массив с границами 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
Единственное, что не конкретизировано в описании этого класса, это реализация программ
Связывание с АТД
Класс, как неоднократно говорилось, является реализацией АТД, заданного формальной спецификацией или неявно подразумеваемого. В начале лекции отмечалось, что утверждения можно рассматривать, как способ введения в класс семантических свойств, лежащих в основе АТД. Давайте уточним наше понимание концепции утверждений, прояснив их связь с компонентами спецификации АТД.
Не просто коллекция функций
Как отмечалось в лекции про АТД, они включают четыре элемента:
