Если Р содержит циклы, то исследование вопросов правильности усложняется, может оказаться вообще невозможным ответшь на ... - Большая Энциклопедия Нефти и Газа
Выдержка из книги
Лингер Р.N.
Теория и практика структурного программирования
Если Р содержит циклы, то исследование вопросов правильности усложняется, может оказаться вообще невозможным ответшь на них. Тот факт, что циклическая программа заканчивается в какой-то мере свидетельствует о ее правильности. Часто уверенность в завершении программы основывается на том, что регулярно изменяющаяся переменная должна в конечном счете вызвать вычисление значения предиката, при котором цикл закончится, или она проистекает из того, что логическая предикатная переменная, которой предварительно присвоено значение истина, после присваивания ей значения ложь обусловливает выход из цикла Однако, даже если провести такое наблюдение невозможно, нельзя сделать вывод о том, что программа зацикливается. Действительно, если выполнение программы Р останавливается при некотором данном начальном значении аргумента из области определения функции, например Л, то логически невозможно ( неразрешимо) определение того, что программа оканчивается вообще.