Формальная модель программ определяется множеством интерпретаций, на которых проводятся вычисления схем программ. Схема программ называется свободной в заданной модели, если любая синтаксически допустимая трасса в схеме программ реализуется вычислением в некоторой интерпретации указанной модели. Свободная схема программ называется вполне свободной, если при переходе от выполнения одного оператора к другому проводится проверка всех логических условий. Формальная модель программ удовлетворяет условию (вполне) свободной схемы, если любая схема программ имеет эквивалентную в данной модели (вполне) свободную схему. Установлено, что условие вполне свободной схемы неравносильно условию свободной схемы. Определены операции расширения формальных моделей за счет введения новых операторов и новых логических условий. В терминах введенных операций расширения моделей установлены необходимые и достаточные признаки, при которых формальная модель удовлетворяет условию вполне свободной схемы. Показано, что класс регулярных формальных моделей программ, интерпретации которого задаются при помощи конечных автоматов, является в определенном смысле минимальным классом моделей, удовлетворяющим условию вполне свободной схемы.

формальная модель программ, схема программ, свободная схема, вполне свободная схема, конечный автомат

Математические вопросы и теория численных методов