Ревизия массивов

Роль процедур создания

Инвариант класса задает множество свойств объектов (экземпляров класса), которые должны выполняться в стабильные времена жизни объектов. В частности, эти свойства должны выполняться сразу после создания экземпляра объекта.

Стандартный механизм распределения инициализирует поля значениями по умолчанию соответствующих типов, приписанных атрибутам. Эти значения могут удовлетворять или не удовлетворять инварианту. Если нет, то требуется специальная процедура создания, инициализирующая значения атрибутов таким образом, чтобы инвариант выполнялся. Поэтому процедуру создания можно рассматривать, как операцию, гарантирующую, что все экземпляры класса начинают жить, имея корректный статус, - в котором инвариант выполняется.

При первом представлении процедур создания они рассматривались, как способ ответа на земной (и очевидный) вопрос, как переопределить инициализацию по умолчанию, если она не подходит для моего класса. Другая рассматриваемая проблема, - как задать несколько различных механизмов инициализации. Но теперь, с введением инвариантов и теоретического обсуждения, отраженного в правиле (1), мы видим более весомую роль процедур создания. Теперь они создают уверенность, что любой экземпляр класса, только начиная жить, удовлетворяет фундаментальным правилам своей касты - инварианту класса.

Набросок библиотечного класса ARRAY дан в предыдущей лекции. Теперь мы в состоянии дать ему подходящее определение. Фундаментальное понятие массива требует задания предусловий, постусловий и инварианта.

Приведем улучшенный, но все еще схематичный вариант, включающий утверждения. Предусловия выражают базисные требования к доступу и модификации элементов: индексы должны быть в допустимой области. Инвариант задает отношение, существующее между count, lower и upper. Компонент count разрешается реализовать функцией, а не задавать атрибутом.

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

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

Дата добавления: 2014-01-07