Здравствуйте, Куть, Вы писали:

К>А может, не нужно перебирать все строки, а можно как-нибудь сгруппировать их? А что, если Анализатор сам этим займётся на основе текста программы парсера, которую подали ему на вход?

Вооот...
Это другой полюс исследований в этой области.

Делается это через "док-ва". В практическом плане на прямо сегодня — через дедукцию и парные ей альфа/бета-редукции. Есть некий набор примитивов, про которые известны их характеристики. Любая программа — комбинация таких примитивов с учетом их ограничений. Св-ва подавляющего большинства однопоточных алгоритмов можно вывести через св-ва их примитивов и способа их комбинации.

Это т.н. "символьные вычисления" — противоположность твоему подходу.


К>Но люди как-то поняли, что она останавливается.

Не как-то, а через упомянутую дедукцию. Были найдены и доказаны св-ва алгоритма для N =0, 1, ... и были выражены св-ва алгоритма для любого N через св-ва алгоритма для (N-1).


К>Я писал про запуск парсера на одной строке, грубо говоря. Это свойство большинства алгоритмов: они не перебирают все возможные состояния, как твоя программа, которая запускает парсер на всех возможных строках.
К>Так какие фундаментальные ограничения у алгоритма?

"Алгоритм" не в состоянии сделать вывод о корректности программы за разумное время. "Алгоритм" может только выдать "да/нет" для конкретного набора входных данных. Чем это лучше запуска целевой программы на этих же данных — я ХЗ, если честно. От того, что мы проэмулировали императивный вычислитель, мы не поменяли низлежащую вычислительную модель; мы лишь, считай, добавили немного отладочной информации. ))