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

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 . Следующий рисунок иллюстрирует этот процесс:

Рис. 11.8. Вычисление цикла (из [М 1990])

Вычисление цикла имеет следующие ингредиенты:

[x].Цель post , определяемую как свойство, выполняемое в любом допустимом заключительном состоянии. Пример: " Result является максимумом массива". На рисунке цель post представлена множеством состояний POST .

[x].Инвариант цикла inv , являющийся обобщением цели, так что можно говорить, что цель - это частный случай инварианта. Пример: " Result является максимумом текущей нарезки массива". Инвариант цикла поиска цели, изображенный на рисунке: "Каждая точка лежит на поверхности, содержащей POST .

[x].Точку инициализации init , о которой известно, что она должна быть в INV , другими словами должна обеспечить выполнение инварианта.

[x].Преобразование body , начинающееся в INV , но не в POST , вырабатывающее точку более близкую к POST , но все еще остающуюся в INV . Тело цикла функции maxarray является примером подобного преобразования.

[x].Верхняя граница числа применений body , необходимого для перевода точки из INV в POST . Как будет пояснено ниже, этот параметр необходим для определения варианта.

Последовательные приближения один из главных инструментов численного анализа. Но там эта идея понимается шире. Важная разница состоит в том, что в чистой математике допускаются бесконечные вычисления, последовательность может иметь предел, даже если он не достигается конечным числом приближений. Последовательность 1/n имеет предел 0 , хотя среди членов последовательности нет числа 0 . В компьютерных вычислениях мы хотим видеть результаты на нашем экране еще при нашей жизни, так что мы настаиваем, все аппроксимирующие последовательности достигают своей цели после конечного числа итераций.