Определение: Вариант цикл

Вариантом цикла является целочисленное выражение, обладающее тремя свойствами.

V1 После выполнения инициализации (предложения from) вариант получает неотрицательное значение.

V2 Каждое выполнение тела цикла (предложения loop), когда условие выхода не выполняется, а инвариант выполняется, уменьшает значение варианта.

V3 Каждое такое выполнение оставляет вариант неотрицательным.

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

В этом доказательстве существенно, что вариант имеет целочисленный тип. Вещественный тип не годится, поскольку можно построить бесконечную уменьшающуюся последовательность, такую как 1, 1/2, 1/3, …, 1/n, … (это строго верно в математике; на компьютере, где бесконечности нет, множество закончилось бы, достигнув "машинного" нуля).

Если вы знаете вариант цикла, синтаксис позволяет вам указать его в предложении variant, следующем после тела цикла. Например, мы можем добавить спецификацию варианта цикла в наше вычислениемаксимума: from

Вариантом является выражение n — i. Он удовлетворяет требуемым условиям.

V1 Инициализация устанавливает i в 1. Предусловие цикла предполагает n ≥ 1. Так что вариант после инициализации неотрицателен.

V2 Тело цикла увеличивает i на единицу, соответственно уменьшая вариант.

V3 Если условие выхода не выполняется, то i будет меньше n (i < n, а не i <= n) и, следовательно, n — i, будучи уменьшенным на единицу, останется неотрицательным.

Из условия V3 следует, что недостаточно рассматривать отрицание условия выхода, которое говорит нам только, что i /= n: нам нужно быть уверенным, что i < n. Заметьте, для этого добавлены новые свойства винвариант цикла: 1 <= i и i <= n. Они выполняются после инициализации цикла и сохраняются при выполнении очередной итерации. Поэтому, когда условие выхода не выполняется, i /= n, то с учетоминварианта i <= n фактически i < n.

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

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