Оператор цикла: базисный синтаксис

Для выражения стратегии цикла в тексте программы будем использовать для нашего примера "максимума" следующую общую структуру:

На данный момент все составляющие операторы являются псевдокодом. Пример демонстрирует три требуемые части конструкции цикла (дополненные позже двумя возможными частями).

• Предложение from вводит операторы инициализации (X1).

• Предложение loop вводит операторы, выполняемые на каждой последовательной итерации (X2).

• Предложение until вводит условие выхода — условие, при котором итерации завершаются (X3).

Эффект выполнения этой конструкции, задаваемой ключевыми словами(from, until, loop), определяется в соответствии с предыдущим обсуждением.

• Первым делом выполняются операторы предложения from (инициализация).

• Пока не выполняется условие выхода в предложении until, выполняются операторы предложения loop (тело цикла).

Более точно это означает, что после инициализации тело цикла может быть выполнено:

• ни разу, если условие выхода из цикла выполняется сразу же после инициализации;

• один раз, если выполнение тела цикла приводит к выполнению условия выхода;

• общая ситуация: i раз для некоторого i, если условие выхода будет ложным для всех j выполнений тела цикла 1 ≤ j < i и становится истинным после i-го выполнения.

Синтаксически предложения from и loop каждое содержат составной оператор. Как следствие, здесь можно использовать произвольное число операторов, в том числе и ноль. Это происходит, например, если цикл не нуждается в явной инициализации (в тех случаях, когда контекст, предшествующий циклу, обеспечивает истинность инварианта цикла); тогда предложение from будет пусто.

From

<------- Здесь ничего

until

— "Условие выхода"

loop

— "Тело цикла"

end

В теле цикла должно быть некое продвижение в процессе аппроксимации (добавить хотя бы один новый элемент к подмножеству предыдущего обсуждения); в противном случае процесс никогда не завершится. Поэтому в реальных программах никогда не встречается цикл с пустым предложением loop.

Включение инварианта

Базисная форма цикла, как мы видели, не показывает инвариант цикла. А жаль, так как инвариант является основой для понимания того, что цикл делает. Поэтому рекомендуемая и возможная форма записи циклавключает предложение invariant. С данным предложением цикл выглядит так:

Инвариант в этом примере — все еще псевдокод, но тем не менее, он полезен, так как поставляет важную информацию о цикле.

Оператор цикла: корректность

Инвариант цикла имеет два важных характеристических свойства.

Корректность

Принцип инварианта цикла

Инвариант цикла должен:

1. стать истинным после инициализации (предложения from);

2. оставаться истинным всякий раз после выполнения тела цикла (предложения loop) в предположении, что значение условия выхода было ложным.

Оператор цикла в результате своего выполнения сохраняет свойство, заданное инвариантом, начиная с удовлетворения свойства, сохраняя свойство после каждой итерации, завершая работу с выполняемым свойством. Это сохранение свойства объясняет полученное им имя "инвариант", применимое здесь к инвариантам цикла (как к ранее инвариантам класса, которые подобным образом должны стать истинными в результате выполнения процедуры создания и оставаться истинными после каждого выполнения метода класса).

Как мы уже видели, цель цикла — в достижении определенного результата путем последовательных аппроксимаций. Шагами, направленными на достижение цели, являются инициализация и последовательное выполнение тела цикла. После каждого из этих шагов свойство устанавливает, что аппроксимация приближает финальный желаемый результат. Инвариант определяет аппроксимацию. В наших двух примерах инвариантами являются:

• , как i-я аппроксимация, для  , финального свойства 

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

Пусть Loop_invariant будет инвариантом. Когда выполнение цикла завершится, инвариант все еще будет выполняться по свойствам I1 и I2 принципа инварианта цикла. Кроме того, условие выхода из циклаLoop_exit также существует, так как в противном случае цикл никогда бы не завершился. Поэтому заключительным условием, истинным в момент завершения, является конъюнкция:

Loop_invariant and Loop_exit

Это условие и определяет результат выполнения цикла.