Трудно отслеживать, что происходит с петлями. Циклы, которые не заканчиваются или не заканчиваются без достижения их целевого поведения, являются распространенной проблемой в компьютерном программировании. Помогают инварианты петли. Инвариант цикла - это формальное утверждение о связи между переменными в вашей программе, которое сохраняется как раз перед тем, как цикл запускается (установление инварианта), и снова становится истинным в нижней части цикла, каждый раз через цикл (поддерживая инвариант ).
Вот общая схема использования инвариантов цикла в вашем коде:
...
// Инвариант цикла должен быть истинным
while (СОСТОЯНИЕ ИСПЫТАНИЯ) {
// вершина цикла
...
// нижняя часть цикла
// Здесь инвариант цикла должен быть истинным
}
// Завершение + Цикл Инвариант = Цель
...
Между верхом и низом петли, по-видимому, продвигается движение к достижению цели петли. Это может нарушить (сделать ложным) инвариант. Суть инвариантов цикла - это обещание, что инвариант будет восстановлен перед повторением тела цикла каждый раз.
В этом есть два преимущества:
Работа не переносится на следующий этап сложными, зависящими от данных способами. Каждый проход по циклу не зависит от всех остальных, а инвариант служит для связывания проходов в рабочее целое.
Рассуждение о том, что ваш цикл работает, сводится к рассуждению о том, что инвариант цикла восстанавливается при каждом прохождении цикла. Это разбивает сложное общее поведение цикла на маленькие простые шаги, каждый из которых может рассматриваться отдельно.
Условие проверки цикла не является частью инварианта. Это то, что заставляет цикл завершаться. Вы рассматриваете отдельно две вещи: почему цикл должен когда-либо завершаться, и почему цикл достигает своей цели, когда завершается. Цикл завершится, если каждый раз через цикл вы будете приближаться к выполнению условия завершения. Это часто легко гарантировать: например, пошаговое изменение переменной счетчика на единицу, пока не будет достигнут фиксированный верхний предел Иногда рассуждение о прекращении труднее.
Инвариант цикла должен быть создан таким образом, чтобы при достижении условия завершения и инварианте true, тогда была достигнута цель:
инвариант + окончание => цель
Требуется практика для создания простых и взаимосвязанных инвариантов, которые охватывают все достижения цели, кроме завершения. Лучше всего использовать математические символы для выражения инвариантов цикла, но когда это приводит к слишком сложным ситуациям, мы полагаемся на ясную прозу и здравый смысл.