Взгляд изнутри

Новое решение упрощает реализацию, также как и улучшает интерфейс. Более важно, дав каждой подпрограмме простую спецификацию, мы смогли сконцентрироваться только на одной задаче. Это позволило избавиться от ненужной избыточности, в частности от лишних циклов. Процедуры вставки и удаления занимаются теперь своей задачей и им не нужно выполнять проход по списку. Ответственность за позиционирование курсора теперь лежит на других подпрограммах ( back, forth, go,search ), только некоторым из которых нужны циклы ( go и search ).

Рис. 5.10.Представление списка с курсором (первый вариант)

В заголовке списка наряду со ссылкой на первый элемент first_element полезно хранить еще две ссылки на элемент в позиции курсора active и предшествующий ему элемент - previous. Это позволит эффективно выполнять вставку и удаление.

Клиенты могут узнать, каково состояние списка, имея доступ к открытым целочисленным атрибутам count и index и булевым запросам: before, after, is_first, is_last, item. Вот две типичные функции:

after: BOOLEAN is

-- Находится ли курсор за списком?

do Result := (index = count + 1) end

is_first: BOOLEAN is

-- Установлен ли курсор на первом элементе?

do Result := (index = 1) end

(Напишите самостоятельно функции before и is_last.) Для функции after высказывание "Стоит ли курсор справа от последнего элемента?" не совсем корректно, так как after может быть истинным, даже если в списке совсем нет элементов. Комментарии к заголовкам следует писать так, чтобы они были ясными; лаконичность и аккуратность - сестры таланта (см. лекцию 8).

Запрос item возвращает элемент в позиции курсора, если таковой имеется:

item: G is

-- Элемент в позиции курсора

require

readable: readable

do

Result := active.item

end

Напоминаю, readable указывает, установлен ли курсор на элементе списка ( index между 1 и count ). Также заметьте,item в active.item ссылается на атрибут в LINKABLE, а не на функцию из самого LINKED_LIST.

Рассмотрим теперь основные команды манипулирования курсором. Обращаться с ними нужно довольно деликатно, в утешение можно заметить, что лишь небольшая их часть - start, forth, put_right, put_left и remove, - выполняет нетривиальные операции над ссылками. Давайте начнем с команд start и forth. Процедура start должна работать как с пустым, так и с не пустым списком. Для пустого списка соглашение состоит в том, что start передвигает курсор ко второму стражу.

start1 is

-- Передвигает курсор к первой позиции.

-- (Предварительная версия.)

do

index := 1

previous := Void

active := first_element

ensure

moved_to_first: index = 1

empty_convention: empty implies after

end

forth1 is

-- Передвигает курсор к следующей позиции.

-- (Предварительная версия.)

require

not_after: not after

do

index := index + 1

if before then

active := first_element; previous := Void

else

check active /= Void end

previous := active; active := active.right

end

ensure

moved_by_one: index = old index + 1

end

Пора остановиться! Все становится слишком сложным и неэффективным. Производительность процедуры forth является критической, поскольку типично она используется клиентом в цикле from start until after loop ...; forth end. Можно ли избавиться от теста?

Можно, если всерьез рассматривать левого стража и всегда создавать его одновременно с созданием списка. (Процедура созданияmake для LINKED_LIST остается в качестве упражнения.) Заменим first_element ссылкой zeroth_element на левого стража:

Рис. 5.11.Представление списка с курсором (пересмотренная версия)

Свойства zeroth_element /= Void и previous /= Void будут теперь частью инварианта (следует, конечно, убедиться, что процедура создания обеспечивает его выполнение). Они весьма ценны, поскольку позволяют избавиться от многих повторяемых проверок.

Процедура forth, запускаемая после обновленной процедуры start, теперь проще и быстрее (без проверок!):

start is

-- Передвигает курсор к первой позиции

do

index := 1

previous := zeroth_element

active := previous.right

ensure

moved_to_first: index = 1

empty_convention: empty implies after

previous_is_zeroth: previous = zeroth_element

end

forth is

-- Передвинуть курсор к следующей позиции.

-- (Версия пересмотрена в интересах эффективности. Без тестов!)

require

not_after: not after

do

index := index + 1

previous := active

active := active.right

ensure

moved_by_one: index = old index + 1

end

Удобно определить go_before, устанавливающую курсор на левом страже:

go_before is

-- Передвигает курсор к before

do

index := 0

previous := zeroth_element

active := zeroth_element

ensure

before: before

previous_is_zeroth: previous = zeroth_element

previous_is_active: active = previous

end

Процедура go определяется в терминах go_before и forth:

go (i: INTEGER) is

-- Передвигает курсор к i-й позиции

require

not_offleft: i >= 0

not_offright: i <= count + 1

do

from

if i < index then go_before end

invariant index <= i variant i - index until index = i loop

forth

end

ensure

moved_there: index = i

end

Мы старательно избегали проходов по списку. Процедуре go, единственной из рассмотренных, необходим цикл. Для симметрии следует добавить finish, перемещающую курсор к последней позиции, реализуемую вызовом go (count + 1).

Хотя и нет настоящей независимости, удобно (Принцип Списка Требований) экспортировать go_before. Тогда для симметрии следует включить и go_after, выполняющую go (count + 1), и экспортировать ее.

Также для симметрии добавлена процедура back, содержащая цикл, подобный go:

back is

-- Передвинуть курсор к предыдущей позиции

require

not_before: not before

do

check index - 1 >= 0 end

go (index - 1)

ensure

index = old index - 1

end

Приятно иметь симметрию между back и forth, однако в ней таится угроза, поскольку клиент может беззаботно вызыватьback, не думая, что ее реализация содержит цикл, в котором index - 1 раз вызывается forth. Если работа с левой частью списка проводится от случая к случаю, то однонаправленный список является подходящим, если же одинаково часто необходимо обращаться к элементам слева и справа от текущего, то необходимо перейти к двунаправленному списку. Соответствующий класс может быть построен как наследник LINKED_LIST (наследование используется корректно, так как двунаправленный список одновременно является и однонаправленным). Создание такого списка оставлено в качестве упражнения (см. У5.7). Следует его выполнить, если хотите достигнуть полного понимания концепций.

Ранние утверждения в инварианте не зависели от реализации. Добавим теперь утверждения, описывающие особенности реализации:

empty = (zeroth_element.right = Void)

zeroth_element /= Void; previous /= Void

(active = Void) = after; (active = previous) = before

(not before) implies (previous.right = active)

(previous = zeroth_element) = (before or is_first)

is_last = ((active /= Void) and then (active.right = Void))

Большинство из запросов реализуются непосредственно - before возвращает булево значение (index = 0) и after - (index = count + 1). Элемент в позиции курсора дается:

item: G is

-- Значение элемента в позиции курсора

require

readable: readable

do

Result := active.item

end

Процедура search подобна go и оставлена читателю. Следует также написать процедуру i_th (i: INTEGER), возвращающую элемент в позиции i. Следует позаботиться об отсутствии абстрактного побочного эффекта, допуская конкретный побочный эффект.

Последняя категория компонентов включает процедуры вставки и удаления:

remove is

-- Удаляет элемент в позиции курсора и передвигает курсор к правому соседу.

-- (Если нет правого соседа, то становится истинным after).

require

readable: readable

do

active := active.right

previous.put_right (active)

count := count - 1

ensure

same_index: index = old index

one_less_element: count = old count - 1

empty_implies_after: empty implies after

end

active := active.right

if previous /= Void then previou.sput_right (active) end

count := count - 1

if count = 0 then

first_element := Void

elseif index = 1 then

first_element := active

-- Иначе first_element не изменяется

end

Утверждения помогают понять намерения и избежать ошибок. Следует поупражняться в овладении этой техникой, написав процедуры put_left и put_right.