Программисты часто составляют циклы, как правило, чтобы достичь какой-то конкретной цели: найти элемент с заданными свойствами, выполнить сортировку и т. п. Но как убедиться в том, что цель будет достигнута, не выполняя цикл непосредственно? В этом нам поможет инвариант цикла.

Инвариант цикла -- это утверждение, относящееся к переменным программы, которое остается истинным в начале и в конце выполнения каждой итерации цикла.

...
// Инвариант цикла должен быть истинным здесь
while ( Условие_выполнения_цикла ) {
    // начало тела цикла
    ...
    // конец тела цикла
    // Инвариант цикла должен быть истинным здесь
}
...

Рассмотрим использование инварианта цикла на примере поиска индекса наименьшего элемента в целочисленном массиве.

Пусть имеется массив a, состоящий из n элементов. Введем переменную TemporarySmallest (индекс элемента, в данный момент являющегося наименьшим) и положим ее равной 0 перед началом проверки. Далее, будем сравнивать a[TemporarySmallest] последовательно с a[1], a[2], ..., a[n-1]. Если окажется, что a[TemporarySmallest] больше какого-либо из a[k], то обновим значение TemporarySmallest. Обозначим переменой nextToCheck индекс элемента, подлежащего проверке.

Инвариант цикла будет выглядеть так:

1. TemporarySmallest находится внутри [0,nextToCheck),
2. и для всех k из [0,nextToCheck) выполняется A[k] >= A[TemporarySmallest].

[a,b) означает: все целые числа, находящиеся на промежутке от a до b, включая a, но не включая b.

Другими словами: наименьший элемент массива с известным индексом TemporarySmallest находится внутри исследованного промежутка [0,nextToCheck). Это утверждение должно оставаться истинным в начале и в конце каждой итерации.

Инициализируем переменные, входящие в инвариант, так, чтобы он был истинным до начала выполнения цикла:

nextToCheck = 1;
TemporarySmallest = 0;

-- индекс наименьшего элемента равен 0, и это единственный элемент в исследованном промежутке [0,1). Пока инвариант сохраняется.

На каждом шаге цикла значение nextToCheck увеличивается на 1, и, при необходимости, изменяется TemporarySmallest:

   if ( a[TemporarySmallest] > a[nextToCheck] ) {
      TemporarySmallest = nextToCheck ;
   }
   nextToCheck++ ;

-- так, чтобы инвариант цикла оставался истинным в конце каждой итерации. Следовательно, и по окончании цикла инвариант сохранится -- наименьший элемент массива с известным индексом TemporarySmallest будет находиться внутри исследованного промежутка [0,nextToCheck).

Условием окончания цикла является отсутствие в массиве a элементов, подлежащих проверке: nextToCheck == n. Таким образом, сохранение инварианта цикла гарантирует нам, что по окончании цикла (исчерпании элементов, подлежащих проверке) будет найден индекс наименьшего элемента TemporarySmallest -- достигнута цель цикла. Это можно записать как

Инвариант цикла && Условие_окончания_цикла => Цель цикла

Вместо условия окончания можно использовать условие выполнения цикла. В нашем случае это: nextToCheck < n (пока есть элементы для проверки). Как только оно будет нарушено (станет ложным), выполнение цикла прекратится

Инвариант цикла && !(Условие_выполнения_цикла) => Цель цикла

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

Заметим, что использование инварианта цикла позволяет рассматривать итерации по отдельности, поскольку каждая из них начинается с одного и того же состояния -- истинности инварианта цикла, и, в этом смысле, не содержит "следов" прошлых итераций. В результате, рассуждения о том, правильно ли работает цикл, сводятся к проверке того, восстанавливается ли истинность инварианта цикла в конце итерации.

Вопросы для самопроверки при составлении циклов:

• Является ли инвариант цикла истинным до начала цикла (инициализированы ли должным образом nextToCheck и TemporarySmallest)?
• Для произвольной итерации: является ли инвариант цикла истинным на входе в тело цикла, и по выходе из него?
• Происходит ли движение по направлению к окончанию выполнения цикла (инкрементируется ли индекс nextToCheck в теле цикла)?
• Приводит ли сохранение инварианта цикла и условия окончания цикла к достижению цели?

При составлении циклов может оказаться удобным понятие области неопределенности, используемое в вычислительных методах математики. Область изменения параметров задачи (в нашем примере: [0,n)) можно разделить на две части: исследованную область (для которой найден TemporarySmallest: [0,nextToCheck)) и область неопределенности ([nextToCheck,n)). Необходимо составлять цикл так, чтобы на каждой итерации область неопределенности сокращалась.

Вернемся к нашему примеру. В начале первой итерации исследованная область представляла собой единственную точку 0, а область неопределенности составляла [1,n). На втором шаге область неопределенности сократилась до [2,n), на третьем -- до [3,n) и т. д., пока, наконец, не превратилась в пустое множество, не содержащее точек.

Рассмотрим еще один пример -- сортировку выбором по убыванию. Пусть, нужно отсортировать массив a из n целых чисел. Найдем наименьший элемент и поместим его в конец массива, на позицию n-1. Затем среди оставшихся элементов вновь выберем наименьший и поместим его на позицию n-2 и т. д. На i-й итерации отсортированные элементы будут занимать позиции от i до n-1, а оставшиеся невыбранными -- от 0 to i-1.

Для поиска наименьшего элемента используем функцию FindMin(int a[], int n), возвращающую индекс наименьшего элемента и написанную на основе рассмотренного выше примера. Введем переменную numSorted, обозначающую количество отсортированных элементов массива.

Инвариант цикла будет таким:

1. numSorted наименьших элементов массива отсортированы в убывающем порядке на промежутке [n-numSorted,n),
2. оставшиеся элементы массива находятся на промежутке [0,n-numSorted).

Непосредственно перед циклом инициализируем значение numSorted:

numSorted = 0;

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

На каждой итерации количество numSorted увеличивается на единицу. Чтобы этого достичь, выбирается наименьший среди первых [0,n-numSorted) неотсортированных элементов, и меняется местами (с помощью функции swap()) c элементом n-numSorted

i = findMinumum(A,n-numSorted);
numSorted++;
swap(A, i, n-numSorted);

Таким образом, отсортированный "хвост" массива всякий раз удлиняется на один элемент, а неотсортированная "голова" уменьшается.

Цикл оканчивается по достижении numSorted == n.

Что почитать

Вирт Н. Алгоритмы + структуры данных = программы

Дейкстра Э. Дисциплина программирования

Кёниг Э., Му Б. Э. Эффективное программирование на C++ (c. 43)

Все есть на Library Genesis.