Синтаксис цикла
Синтаксис цикла непосредственно следует из предшествующих соображений, определяющих ингредиенты цикла. Он будет включать элементы, отмеченные как необходимые.
- Инвариант цикла inv - утверждение.
- Условие выхода exit, чья конъюнкция с inv дает желаемую цель.
- Вариант var - целочисленное выражение.
- Множество инструкций инициализации, которые всегда приводят к состоянию, в котором inv выполняется, а var становится неотрицательным.
- Множество инструкций body, которое (при условии, что оно начинается в состоянии, где var неотрицательно и выполняется inv), сохраняет инвариант и уменьшает var, в то же время следя за тем, чтобы оно не стало меньше нуля.
- Синтаксис цикла честно комбинирует эти ингредиенты:
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 являются возможными. Когда они присутствуют, то помогают прояснить цель цикла и проверить его корректность.Для любого не тривиального цикла характерны интересные варианты и инварианты; многие из примеров в последующих лекциях включают варианты и инварианты, обеспечивая глубокое понимание корректности лежащих в основе алгоритмов.