Ревизия массивов
Роль процедур создания
Инвариант класса задает множество свойств объектов (экземпляров класса), которые должны выполняться в стабильные времена жизни объектов. В частности, эти свойства должны выполняться сразу после создания экземпляра объекта.
Стандартный механизм распределения инициализирует поля значениями по умолчанию соответствующих типов, приписанных атрибутам. Эти значения могут удовлетворять или не удовлетворять инварианту. Если нет, то требуется специальная процедура создания, инициализирующая значения атрибутов таким образом, чтобы инвариант выполнялся. Поэтому процедуру создания можно рассматривать, как операцию, гарантирующую, что все экземпляры класса начинают жить, имея корректный статус, - в котором инвариант выполняется.
При первом представлении процедур создания они рассматривались, как способ ответа на земной (и очевидный) вопрос, как переопределить инициализацию по умолчанию, если она не подходит для моего класса. Другая рассматриваемая проблема, - как задать несколько различных механизмов инициализации. Но теперь, с введением инвариантов и теоретического обсуждения, отраженного в правиле (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 . Поскольку эффективная манипуляция с массивом требует доступа к системам низкого уровня, то эти программы будут реализованы с использованием внешних классов, что будет рассмотрено в последующих лекциях.