Ревизия массивов
Ревизия массивов
Набросок библиотечного класса 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. Поскольку эффективная манипуляция с массивом требует доступа к системам низкого уровня, то эти программы будут реализованы с использованием внешних классов, что будет рассмотрено в последующих лекциях.