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

Синтаксис цикла

Синтаксис цикла

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

[x]. Инвариант цикла inv - утверждение.

[x]. Условие выхода exit, чья конъюнкция с inv дает желаемую цель.

[x]. Вариант var - целочисленное выражение.

[x]. Множество инструкций инициализации, которые всегда приводят к состоянию, в котором inv выполняется, а var становится неотрицательным.

[x]. Множество инструкций body, которое (при условии, что оно начинается в состоянии, где var неотрицательно и выполняется inv), сохраняет инвариант и уменьшает var, в то же время следя за тем, чтобы оно не стало меньше нуля.

[x]. Синтаксис цикла честно комбинирует эти ингредиенты:

from
init
invariant
inv
variant
var
until
exit
loop
body
end

Предложения invariant и variant являются возможными. Предложение from по синтаксису требуется, но инструкция init может быть пустой.

Эффект выполнения цикла можно описать так: вначале выполняется init, затем 0 или более раз выполняется тело цикла, которое перестает выполняться, как только exit принимает значение false.

В языках Pasal, C и других такой цикл называется "циклом while", в отличие от цикла типа "repeat ... until", в котором тело цикла выполняется, по меньшей мере, один раз. Здесь же тест является условием выхода, а не условием продолжения, и синтаксис цикла явно содержит фазу инициализации. Потому эквивалент записи нашего цикла на языке Pascal выглядит следующим образом:

init;
while not exit do body

С вариантами и инвариантами цикл для maxarray выглядит так:

from
i := t.lower; Result := t @ lower
invariant
-- Result является максимумом нарезки массива t в интервале [t.lower,i].
variant
t.lower - i
until
i = t.upper
loop
i := i + 1
Result := Result.max (t @ i)
End

Заметьте, инвариант цикла выражен неформально, в виде комментария. Последующее обсуждение в этой лекции объяснит это ограничение языка утверждений.

Вот еще один пример, ранее показанный без вариантов и инвариантов. Целью следующей функции является вычисление наибольшего общего делителя - НОД (gcd - greatest common divisor) двух положительных целых a и b, следуя алгоритму Эвклида:

gcd (a, b: INTEGER): INTEGER is
-- НОД a и b
require
a > 0; b > 0
local
x, y: INTEGER
do
from
x := a; y := b
until
x = y
loop
if x > y then x := x - y else y := y - x end
end
Result := x
ensure
-- Result является НОД a и b
end

Как узнать, что функция gcd удовлетворяет своему постусловию и действительно вычисляет наибольший общий делитель a и b? Для проверки этого следует заметить, что следующее свойство истинно после инициализации цикла и сохраняется на каждой итерации:

x > 0; y > 0
-- Пара <x, y> имеет тот же НОД, что и пара <a, b>

Это и будет служить инвариантом цикла inv. Ясно, что inv выполняется после инициализации. Если выполняется inv и условие цикла x /= y, то после выполнения тела цикла:

if x > y then x := x - y else y := y - x end

инвариант inv остается истинным, замена большего из двух положительных неравных чисел их разностью не меняет их gcd и оставляет их положительными. Тогда по завершению цикла следует:

x = y and «Пара <x, y> имеет тот же НОД, что и пара <a, b>»

Отсюда, в свою очередь, следует, что x является наибольшим общим делителем. По определению НОД (x, x) = x.

Как узнать, что цикл всегда завершается? Необходим вариант. Если x больше чем y, то в теле цикла x заменяется разностью x-y. Если y больше x, то y заменяется разностью y-x. Нельзя в качестве варианта выбрать ни x, ни y, поскольку для каждого из них нет гарантии уменьшения. Но можно быть уверен, что максимальное из них обязательно будет уменьшено. Поэтому разумно выбрать в качестве варианта x.max(y). Заметьте, вариант всегда остается положительным. Теперь можно написать цикл со всеми предложениями:

from
x := a; y := b
invariant
x > 0; y > 0
-- Пара <x, y> имеет тот же НОД, что и пара <a, b>
variant
x.max (y)
until
x = y
loop
if x > y then x := x - y else y := y - x end
end

Как отмечалось, предложения invariant и variant являются возможными. Когда они присутствуют, то помогают прояснить цель цикла и проверить его корректность. Для любого нетривиального цикла характерны интересные варианты и инварианты; многие из примеров в последующих лекциях включают варианты и инварианты, обеспечивая глубокое понимание корректности лежащих в основе алгоритмов.

Оглавление книги