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

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

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

indexing

description: " Последовательности значений одного типа или %

%согласованных типов, доступных по индексам - целым из заданного интервала %"

class ARRAY [G] creation

make

feature - Initialization (Инициализация)

make (minindex, maxindex: INTEGER) is

-- Создать массив с границами minindex и maxindex

-- (пустой если minindex & gt; maxindex).

require

meaningful_bounds: maxindex & gt; = minindex - 1

do

...

ensure

exact_bounds_if_non_empty: (maxindex & gt; = minindex) implies

((lower = minindex) and (upper = maxindex))

conventions_if_empty: (maxindex & lt; 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 & lt; = i

index_not_too_large: i & lt; = upper

do... end

feature -- Element change (Изменение элементов)

put (v: G; i: INTEGER) is

-- Присвоить v элементу с индексом i

require

index_not_too_small: lower & lt; = i

index_not_too_large: i & lt; = upper

do

...

ensure

element_replaced: item (i) = v

end

invariant

consistent_count: count = upper - lower + 1

non_negative_count: count & gt; = 0

end

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

Связывание с АТД

Класс, как неоднократно говорилось, является реализацией АТД, заданного формальной спецификацией или неявно подразумеваемого. В начале лекции отмечалось, что утверждения можно рассматривать, как способ введения в класс семантических свойств, лежащих в основе АТД. Давайте уточним наше понимание концепции утверждений, прояснив их связь с компонентами спецификации АТД.