Определения: логический алгоритм, вычисление, производимые вычисления, завершаемость, критерий для верификации программы.

Логический алгоритм – получается в рез-те выбора некоторой управл.

стратегии С для выполнения программы (P,G) и обознач-ся (P,G,C).

Целью исполнения программы явл. порождение вычислений Г. Каждое

вычисление представляет собой послед-ть целей, начинающиеся с

исходной программы G.

Вычисление Г явл. производимым из программы (P,G) при управл-ии С

тогда и только тогда, когда исполнение (P,G,C) порождает цель из Г за

конечное число шагов.

Завершаемость – предпологает единств. возможное вычисление и программа завершается в том случае, когда это вычисление конечное.

Критерий для верификации программы: