Cтраница 4
Конечно, пошаговый транслятор работает медленнее, но зато существенно упрощается и ускоряется работа пользователя по отладке синтаксиса своей программы. Так что замедление работы транслятора окупается дополнительными удобствами для пользователей и сокращением общего числа трансляций, необходимых для получения правильной программы. [46]
Указанные теоретические препятствия не должны, конечно, удерживать нас от попыток построить автоматические и полуавтоматические средства верификации логических программ, поскольку для подавляющего большинства практически действующих программ вполне возможно доказать их правильность ( или неправильность) с помощью систематических и эффективных аналитических методов. Помимо этого, важно также осознавать, что приведенные здесь критерии правильности можно рассматривать как условия, управляющие синтезом необходимо правильных программ. Использование проверенных синтезирующих систем, основанных на этих критериях, позволяет эффективным образом избавиться от рассмотрения вообще всех неправильных программ, и тем самым мы в значительной степени преодолеваем ограничения разрешимости, которые потенциально оказывают влияние на логический анализ произвольно построенных программ. Более подробно вопросы синтеза программ рассматриваются в следующей главе. [47]
Предположим, мы хотим изменить компилятор Си, чтобы включить управляющую последовательность v для представления символа вертикальной табуляции. Ясно, что, поскольку компилятор Си в готовом виде ничего не знает о v, исходная программа не является правильной программой на языке Си. Заглянув в таблицу кодировки символов ASC II, мы находим, что код вертикальной табуляции - десятичное И. Мы изменяем нашу исходную программу, как показано на рис. 2.3. Теперь старый компилятор компилирует новый исходный текст без ошибок. [48]