Основы объектно-ориентированного программирования

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.

Это пример вычисления последовательными приближениями. Мы продвигаемся вверх по массиву