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

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

[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 являются возможными. Когда они присутствуют, то помогают прояснить цель цикла и проверить его корректность. Для любого нетривиального цикла характерны интересные варианты и инварианты; многие из примеров в последующих лекциях включают варианты и инварианты, обеспечивая глубокое понимание корректности лежащих в основе алгоритмов.