BS1
from
i := 1; j := n
until i = j loop
m := (i + j) // 2
if t @ m <= x then
i := m
else
j := m
end
end
Result := (x = t @ i)
BS2
from
i := 1; j := n; found := false
until i = j and not found loop
m := (i + j) // 2
if t @ m < x then
i := m + 1
elseif t @ m = x then
found := true
else
j := m - 1
end
end
Result := found
BS3
from
i := 0; j := n
until i = j loop
m := (i + j + 1) // 2
if t @ m <= x then
i := m + 1
else
j := m
end
end
if i >= 1 and i <= n then
Result := (x = t @ i)
else
Result := false
end
BS4
from
i := 0; j := n + 1
until i = j loop
m := (i + j) // 2
if t @ m <= x then
i := m + 1
else
j := m
end
end
if i >= 1 and i <= n then
Result := (x = t @ i)
else
Result := false
end
Таблица 11.3.Четыре (ошибочных) попытки реализации бинарного поиска
Сделаем циклы корректными
Разумное использование утверждений может помочь справиться с такими проблемами. Цикл может иметь связанное с ним утверждение, так называемый инвариант цикла (loop invariant), который не следует путать с инвариантом класса. Он может также иметь вариант цикла (loop variant), являющийся не утверждением, а, обычно целочисленным выражением. Совместно, инвариант и вариант позволяют гарантировать корректность цикла.
Для понимания этих понятий необходимо осознать, что цикл - это способ вычислить некоторый результат последовательными приближениями (successive approximations).
Рассмотрим тривиальный пример вычисления максимума в целочисленном массиве, используя очевидный алгоритм:
maxarray (t: ARRAY [INTEGER]): INTEGER is
-- Максимальное значение массива t
require
t.capacity >= 1
local
i: INTEGER
do
from
i := t.lower
Result := t @ lower
until i = t.upper loop
i := i + 1
Result := Result.max (t @ i)
end
end
В разделе инициализации i получает значение нижней границы массива, а сущность Result - будущий результат вычислений - значение первого элемента. Предусловие гарантирует существование хотя бы одного элемента в массиве. Производя последовательные итерации в цикле, мы достигаем верхней границы массива, увеличивая на каждом шаге i на 1, и заменяя Result значением элемента t @ i, если этот элемент больше чем Result. Для нахождения максимума двух целых используется функция max, определенная для класса integer: a.max(b) возвращает максимальное значение из a и b.
Это пример вычисления последовательными приближениями. Мы продвигаемся вверх по массиву последовательными нарезками: [lower, lower], [lower, lower+1], [lower, lower+2] и так вплоть до полного приближения [lower, upper].
Свойство инварианта цикла состоит в том, что на каждом шаге прохождения цикла Result представляет максимум текущей нарезки массива. Инициализация гарантирует выполнимость этого свойства непосредственно перед началом работы цикла. Каждая итерация увеличивает нарезку, сохраняя истинность инварианта. Цикл завершает свою работу, когда очередная нарезка массива совпадает со всем массивом. В этом состоянии истинность инварианта означает, что Result является максимумом массива, что и является требуемым результатом работы.
Рис. 11.7. Аппроксимация массива последовательными нарезками
Ингредиенты доказательства корректности цикла
Простой пример вычисления максимума массива иллюстрирует общую схему циклических вычислений, применимую ко многим ситуациям. Вы определяете, что решением некоторой проблемы является элемент, принадлежащий n-мерной поверхности POST. В некоторых случаях POST может содержать ровно один элемент - решение, но обычно может быть более чем одно приемлемое решение проблемы. Циклы полезны, когда нет прямого способа достичь решения "одним выстрелом". Но у вас есть непрямая стратегия, вы можете, например, прицелиться и попасть в m-мерную поверхность INV, включающую POST (для m>n). Инвариантом является то, что поверхность попадания все время содержит POST. Итерация за итерацией приближаемся к POST, сохраняя истинность INV. Следующий рисунок иллюстрирует этот процесс: