Бинарный поиск - один из ключевых элементов базового курса "Введение в информатику" (Computer Science 101) - хорошая иллюстрация "коварства" циклов даже в относительно тривиальной ситуации. Рассмотрим целочисленный, упорядоченный по возрастанию массив t с индексами от 1 до n. Используем алгоритм бинарного поиска для ответа на вопрос: появляется ли целое x среди элементов массива. Если массив пуст, ответ должен быть "нет", если в массиве ровно один элемент, то ответ "да" тогда и только тогда, когда элемент массива совпадает с x. Суть бинарного поиска, использующего упорядоченность массива, проста: вначале x сравнивается со средним элементом массива, если есть совпадение, то задача решена, если x меньше среднего элемента, то поиск продолжается в верхней половине массива, в противном случае - в нижней половине. Каждое сравнение уменьшает размер массива вдвое. Ниже представлены четыре попытки реализации этой простой идеи. К несчастью, все они содержат ошибки. Вам предоставляется случай поупражняться в поиске ошибок и установить, в какой ситуации каждый из алгоритмов не работает нужным образом.
| Напомню, t @ m означает элемент массива t с индексом m. Знак операции // означает деление нацело, так что 7 // 2 и 6 // 2 дают значение 3. Синтаксис цикла будет дан ниже, но он должен быть и так понятен. Предложение from вводит инициализацию цикла. |
| 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.Четыре (ошибочных) попытки реализации бинарного поиска
<p>Сделаем циклы корректными</p>Разумное использование утверждений может помочь справиться с такими проблемами. Цикл может иметь связанное с ним утверждение, так называемый инвариант цикла (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.
