Один из способов доказать остановку цикла - определить некоторую целочисленную переменную (не обязательно явно в программе), которая всегда уменьшается при каждом выполнении цикла, и что как только эта переменная станет меньше нуля, цикл завершится. Мы можем назвать эту переменную вариантом цикла.
Рассмотрим следующий небольшой фрагмент:
var x := 20;
while (x >= 0) {
x := x - 1
}
Здесь мы видим, что x уменьшается каждый раз при выполнении цикла, и что цикл завершится после x ‹0 (очевидно, это не очень строго, но вы поняли идею). Следовательно, мы можем использовать x как вариант.
А как насчет более сложного примера? Рассмотрим конечный список целых чисел 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, и поэтому цикл завершится.
person
Michael Williamson
schedule
18.03.2010
