![]() Главная страница Случайная страница КАТЕГОРИИ: АвтомобилиАстрономияБиологияГеографияДом и садДругие языкиДругоеИнформатикаИсторияКультураЛитератураЛогикаМатематикаМедицинаМеталлургияМеханикаОбразованиеОхрана трудаПедагогикаПолитикаПравоПсихологияРелигияРиторикаСоциологияСпортСтроительствоТехнологияТуризмФизикаФилософияФинансыХимияЧерчениеЭкологияЭкономикаЭлектроника |
Синтаксис цикла
Синтаксис цикла непосредственно следует из предшествующих соображений, определяющих ингредиенты цикла. Он будет включать элементы, отмеченные как необходимые. [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 & gt; 0; b & gt; 0 local x, y: INTEGER do from x: = a; y: = b until x = y loop if x & gt; y then x: = x - y else y: = y - x end end Result: = x ensure -- Result является НОД a и b end
Как узнать, что функция gcd удовлетворяет своему постусловию и действительно вычисляет наибольший общий делитель a и b? Для проверки этого следует заметить, что следующее свойство истинно после инициализации цикла и сохраняется на каждой итерации:
x & gt; 0; y & gt; 0 -- Пара & lt; x, y& gt; имеет тот же НОД, что и пара & lt; a, b& gt;
Это и будет служить инвариантом цикла inv. Ясно, что inv выполняется после инициализации. Если выполняется inv и условие цикла x /= y, то после выполнения тела цикла:
if x & gt; y then x: = x - y else y: = y - x end
инвариант inv остается истинным, замена большего из двух положительных неравных чисел их разностью не меняет их gcd и оставляет их положительными. Тогда по завершению цикла следует:
x = y and «Пара & lt; x, y& gt; имеет тот же НОД, что и пара & lt; a, b& gt;»
Отсюда, в свою очередь, следует, что 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 & gt; 0; y & gt; 0 -- Пара & lt; x, y& gt; имеет тот же НОД, что и пара & lt; a, b& gt; variant x.max (y) until x = y loop if x & gt; y then x: = x - y else y: = y - x end end
Как отмечалось, предложения invariant и variant являются возможными. Когда они присутствуют, то помогают прояснить цель цикла и проверить его корректность. Для любого нетривиального цикла характерны интересные варианты и инварианты; многие из примеров в последующих лекциях включают варианты и инварианты, обеспечивая глубокое понимание корректности лежащих в основе алгоритмов.
|