Корректность
Принцип постусловия цикла
Условие, достижимое в результате выполнения цикла, представляет конъюнкцию инварианта и условия выхода.
Синтаксис подчеркивает эту связь — принцип постусловия цикла, — размещая предложения invariant и until друг за другом. Так что, если вы видите инвариант цикла и хотите знать, каков достигнут результат, просто посмотрите на два рядом идущих условия:
Рис. 7.7.
В примере с линией метро неформально условие выхода говорит: "все станции посещены". Конъюнкция этого условия с инвариантом говорит нам, что красная точка отображалась на всех станциях.
Принцип постусловия цикла является прямым следствием определения цикла как механизма аппроксимации. Цитируя предыдущее обсуждение, напомним, что идея состояла в выборе инварианта как некоторого обобщения цели:
"достаточно слабого, чтобы его можно было применить к некоторому начальному подмножеству всего множества": в этом роль инициализации;
"достаточно гибкого, чтобы позволять расширять множество, сохраняя его истинность": в этом роль тела цикла, выполняемого при истинности инварианта и ложности условия выхода из цикла. Тело цикладолжно обеспечить расширение множества и сохранение инварианта;
"достаточно сильного, чтобы из него следовала цель Post, когда он выполняется на всем множестве": это достигается на выходе, когда в соответствии с принципом постусловия цикла становится истинной конъюнкция условия выхода и инварианта.
Завершение цикла и проблема остановки
Согласно описанной схеме выполнения цикла тело цикла выполняется до тех пор, пока не будет выполнено условие выхода. Если цикл строится в соответствии с рассмотренной стратегией аппроксимации, то его выполнение завершится, так как рассматривается конечное множество данных, на каждом шаге происходит расширение подмножества хотя бы на один элемент, потому за конечное число шагов процесс обязательно завершится. Но синтаксис цикла допускает произвольную инициализацию, произвольное тело цикла и условие выхода, так что цикл может никогда не завершиться, как в этом примере:
from
— "Любой оператор (возможно, пусто)"
until
0 /= 0
loop
— "Любой оператор (возможно, пусто)"
end
В этом искусственном, но допустимом примере, условие цикла — которое, конечно, можно просто записать как False, — никогда не выполнится, так что цикл не может завершиться. Если запустить эту программу на компьютере, можно долго сидеть у экрана, где ничего не происходит, хотя компьютер работает. Осознав, что происходит что-то неладное, вы придете к решению, что нужно прервать выполнение (в EiffelStudio для этого есть специальная кнопка). Но у вас нет способа узнать — если вы пользователь программы и не имеете доступа к ее тексту, — "зациклилась" ли программа или просто идут долгие вычисления.
Если программа не завершается, то, хочу напомнить, это еще не является свидетельством ошибочного поведения. Некоторые программы проектируются специально так, чтобы они всегда работали, пока не будут явно остановлены. Прекрасным примером является операционная система (ОС), установленная на компьютере. Я был бы весьма разочарован, если бы при наборе этого текста произошло завершение работы ОС, которое бы означало, что система "рухнула" или я случайно нажал ногой кнопку выключения компьютера. Такая же ситуация существует с большинством "встроенных систем" (программ, выполняемых на различных устройствах): вы не захотите завершения программы мобильного телефона во время вашего разговора.
Но с другой стороны, обычные программы — в частности, большинство программ, обсуждаемых в этой книге, — устроены так, что, получив некоторый ввод, они вырабатывают результат за конечное число шагов.
Когда пишутся такие программы, можно непреднамеренно построить цикл, условие выхода из которого не будет выполняться, что приведет к тому, что вся программа не завершится. Чтобы избежать этого неприятного результата, лучший способ, позволяющий убедиться, что цикл завершится, состоит во введении для каждого цикла элемента, называемого вариантом цикла.