§ 50. Инвариант цикла

Определения и обозначения

Цикл — фрагмент алгоритма, в котором одна и та же последовательность команд многократно выполняется по условию. Он нужен, чтобы не записывать одинаковые действия много раз, например сложение элементов массива.

Итерация — одно выполнение тела цикла. Подсчёт итераций помогает понять, сколько раз обработаны данные и в какой момент меняются управляющие переменные.

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

Условие завершения — условие, при наступлении которого цикл прекращает выполнение. Его рассматривают вместе с инвариантом, чтобы перейти от промежуточного свойства к окончательному ответу.

Как это устроено

Утверждение-инвариант выбирают так, чтобы оно описывало состояние уже обработанной части данных перед каждой итерацией. Например, в цикле суммирования оно может связывать счётчик с суммой всех чисел, которые уже пройдены. Такое утверждение не должно сразу повторять конечный ответ, иначе его нельзя будет использовать для описания промежуточных шагов.

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

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

После выхода из цикла используют одновременно инвариант и условие завершения. Например, инвариант может говорить, что обработаны первые k элементов, а условие выхода — что k равно размеру массива; значит, обработаны все элементы. Но это ещё не гарантирует выхода: нужно отдельно убедиться, что счётчик или другая управляющая величина меняется в правильном направлении и цикл не может выполняться бесконечно.

Этапы доказательства правильности цикла с помощью инварианта

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

Разбор задач

Сумма первых n натуральных чисел

Условие. Цикл должен вычислить сумму 1 + 2 + ... + n. Пусть k — число уже обработанных слагаемых, а s — накопленная сумма.

1. Выберем инвариант: после обработки чисел от 1 до k выполнено s = 1 + 2 + ... + k. До начала k = 0 и s = 0, поэтому инвариант верен для пустой суммы.
2. За итерацию увеличиваем k на 1 и прибавляем k к s. Если до шага s равно сумме до старого k, то после шага оно равно сумме до нового k, значит, инвариант сохраняется.
3. Когда k = n, условие завершения выполнено, а инвариант даёт s = 1 + 2 + ... + n. Счётчик увеличивается на единицу и ограничен значением n, поэтому цикл остановится.

Ответ. Алгоритм корректен: после остановки переменная s содержит сумму первых n натуральных чисел.

Последовательный поиск максимума

Условие. Требуется найти наибольший элемент массива, просматривая его слева направо. Переменная max хранит текущий максимум, а i указывает границу обработанного фрагмента.

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

Ответ. Значение max после выхода из цикла является максимальным элементом массива.

Алгоритм Евклида

Условие. Для натуральных чисел a и b алгоритм заменяет пару (a, b) на (b, a по модулю b), пока b не станет равным нулю. Нужно найти НОД исходных чисел.

1. Инвариант утверждает, что НОД текущей пары равен НОД исходной пары. Он верен в начале, поскольку текущие значения совпадают с исходными.
2. Замена сохраняет НОД: НОД(a, b) = НОД(b, a по модулю b). Следовательно, после каждой итерации инвариант остаётся истинным.
3. При b = 0 НОД(a, 0) равен a, поэтому по инварианту a есть искомый НОД. Остаток уменьшается и в конечном счёте становится нулём, что доказывает остановку.

Ответ. После завершения алгоритма первое число содержит НОД исходной пары.

Типичные ошибки

Инвариант формулируют как конечный результат алгоритма, хотя он должен описывать промежуточное состояние на каждой итерации. Так происходит, когда ученик не учитывает уже обработанную часть данных. Проверка: можно ли применить утверждение до завершения цикла и связать его с текущим счётчиком?

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

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

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

Связь с другими темами

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

Что запомнить

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