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

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

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

Инициализация

До первого повторения утверждение должно быть истинно. Для поиска максимума это может быть фраза: «currentMax равен максимуму уже просмотренного префикса». Тогда переменную инициализируют первым элементом, а просмотренный префикс действительно содержит один элемент.

Сохранение

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

Завершение

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

Ошибка на единицу

Фразы «обработаны элементы до i» и «обработаны элементы по i включительно» задают разные границы. Их нужно согласовать с начальным индексом и моментом увеличения счётчика. Таблица состояния до и после одной итерации помогает обнаружить несоответствие без запуска программы.

Экзаменационная запись

Сформулируйте инвариант одним предложением, затем отдельно обоснуйте базу, сохранение и выход. Для примера найдите состояние, на котором неверный вариант инварианта ломается. Такая структура сильнее комментария «цикл очевидно находит ответ» и подготавливает к уточняющим вопросам комиссии.

Инвариант связывает код с математическим утверждением

Для поиска максимума естественный инвариант звучит так: перед итерацией best равен максимуму уже обработанного префикса. Инициализация первым элементом делает утверждение истинным для префикса длины один; сравнение с очередным значением сохраняет его; после обработки всего списка префикс совпадает со входом.

def maximum(values: list[int]) -> int:
    if not values:
        raise ValueError("empty sequence")
    best = values[0]
    for index in range(1, len(values)):
        if values[index] > best:
            best = values[index]
    return best

assert maximum([-7, -2, -9]) == -2

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

Практика: второй максимум без сортировки

Найдите два наибольших различных значения за один проход. Сначала сформулируйте инвариант для пары best и second, затем решите, что делать с повтором максимума и списком без двух различных чисел. Напишите реализацию и тесты для возрастающей, убывающей, отрицательной и постоянной последовательностей. Вручную составьте трассировочную таблицу: после каждой позиции укажите обработанный префикс и значения обеих переменных.