Один из способов доказать останов цикла - это определить некоторую целочисленную переменную (не обязательно явную в программе), которая всегда уменьшается при каждом выполнении цикла, и, когда эта переменная меньше нуля, цикл завершается. Мы можем назвать эту переменную вариантом цикла.
Рассмотрим следующий небольшой фрагмент:
var x := 20;
while (x >= 0) {
x := x - 1
}
Здесь мы можем видеть, что x уменьшается при каждом выполнении цикла и что цикл завершится, как только x <0 (очевидно, это не очень строго, но вы поняли идею). Следовательно, мы можем использовать x как вариант. </p>
А как насчет более сложного примера? Рассмотрим конечный список целых чисел, L = [L [0], L [1], ..., L [n]]. in(L, x) верно, если x является членом L. Теперь рассмотрим следующую программу:
var x := 0;
while (in(L, x)) {
x := x + 1
}
Это выполнит поиск по натуральным числам (0, 1, 2, ...) и остановится, когда найдет значение для x, которого нет в L. Итак, как мы докажем, что это заканчивается? В L есть максимальное значение - назовите его max (L). Затем мы можем определить наш вариант как max(L) - x. Чтобы доказать завершение, мы должны сначала доказать, что max(L) - x всегда уменьшается - не слишком сложно, поскольку мы можем доказать, что x всегда увеличивается. Затем мы должны доказать, что цикл прекратится, когда max(L) - x < 0. Если max(L) - x < 0, то max(L) < x, что означает, что x не может быть в L, и поэтому цикл завершится.