6.5. «Часовые»

Следующий раздел не касается языков программирования как таковых; ско­рее, он предназначен для того, чтобы показать, что программу можно улуч­шить за счет более совершенных алгоритмов и методов программирования, не прибегая к «игре» на языковых частностях. Этот раздел включен в книгу, по­тому что тема выхода из цикла при последовательном переборе является пред­метом интенсивных дебатов, однако существует и другой алгоритм, который является одновременно ясным, надежным и эффективным.

В последнем примере предыдущего раздела (поиск в массиве) есть три ко­манды перехода в каждой итерации цикла: условный переход цикла for, услов­ный переход if-оператора и переход от конца цикла обратно к началу. Пробле­ма поиска в данном случае состоит в том, что мы проверяем сразу два условия: найдено ли значение key и достигнут ли конец массива? Используя «часового» (sentinel) *, мы можем два условия заменить одним. Идея состоит в том, чтобы ввести в начале массива дополнительно еще один элемент («часового») и хра­нить в нем эталонное значение key, которое нужно найти в массиве (рис. 6.4).

Поскольку мы обязательно найдем key либо как элемент массива, либо как искусственно введенный элемент, постольку достаточно проверять только од­но условие внутри цикла:

Ada

type А_Туре is array(0 .. 100) of Integer;

-- Дополнительное место в нулевой позиции для «часового»

function Find_Key(A: A_Type; Key: Integer)

return Integer is

I: Integer := 100; -- Поиск с конца

begin

A(0) := Key; -- Установить «часового»

while A(l) /= Key loop

I:=I-1;

end loop;

return I;

end Find_Key;

Если при возврате управления из функции значение I равно нулю, то Key в

массиве нет; в противном случае I содержит индекс найденного значения.

Этот код более эффективен, цикл чрезвычайно прост и может быть легко про-

верен.

6.6. Инварианты

Формальное определение семантики операторов цикла базируется на кон­цепции инварианта: формулы, которая остается истинной после каждого вы­полнения тела цикла. Рассмотрим предельно упрощенную программу для вы- числения целочисленного деления а на b с тем, чтобы получить результат у:

у = 0;

C

х = а;

while (х >- b) { /* Пока b «входит» в х, */

х -= b; /* вычитание b означает, что */

у++; /* результат должен быть увеличен */

}

и рассмотрим формулу:

a = yb +х

где курсивом обозначено значение соответствующей программной перемен­ной. После операторов инициализации она, конечно, будет правильной, по­скольку у = 0 и х = а. Кроме того, в конце программы формула определяет, что у есть результат целочисленного деления а/b при условии, что остаток х мень­ше делителя b.

Не столь очевидно то, что формула остается правильной после каждого выполнения тела цикла. В такой тривиальной программе этот факт легко уви­деть с помощью простой арифметики, изменив значения х и у в теле цикла:

(у + \)b + (х-b)=уb+b+х-b=уb+х=а

Таким образом, выполнение тела цикла переводит программу из состояния, которое удовлетворяет инварианту, в другое состояние, которое по-прежнему удовлетворяет инварианту.

Теперь заметим: для того чтобы завершить цикл, булево условие в цикле while должно иметь значение False, то есть вычисление должно быть в таком состоянии, при котором --(х > b), что эквивалентно х < b. Объединив эту фор­мулу с инвариантом, мы показали, что программа действительно выполняет целочисленное деление.

Точнее, если программа завершается, то результат является правильным. Это называется частичной правильностью. Чтобы доказать полную правиль­ность, мы должны также показать, что цикл завершается.

Это делается следующим образом. Так как во время выполнения програм­мы b является константой (и предполагается положительной!), нам нужно по­казать, что неоднократное уменьшение х на b должно, в конечном счете, при­вести к состоянию, в котором 0 < х < b. Но 1) поскольку х уменьшается неод­нократно, его значение не может бесконечно оставаться больше значения b; 2) из условия завершения цикла и из вычисления в теле цикла следует, что х никогда не станет отрицательным. Эти два факта доказывают, что цикл дол­жен завершиться.

Инварианты цикла в языке Eiffel

Язык Eiffel имеет в себе средства для задания контрольных утверждений вооб­ще (см. раздел 11.5) и инвариантов циклов в частности:

from

у = 0; х = а;

invariant

Eiffel

а = yb + х

variant

х

until

x< b

loop

x :=x-b;

у:=у+1;

end

Конструкция from устанавливает начальные условия, конструкция until зада­ет условие для завершения цикла, а операторы между loop и end образуют те­ло цикла. Конструкция invariant определяет инвариант цикла, а конструкция variant определяет выражение, которое будет уменьшаться (но останется неот­рицательным) с каждой итерацией цикла. Правильность инварианта проверя­ется после каждого выполнения тела цикла.