Введен класс математических моделей программ, описываемый в терминах языкового каркаса, который базируется на языке охраняемых команд Э. Дейкстры. Определены модели вычислений, названные авторами системами правил перехода. В терминах этих систем описана семантика программ и дана строгая постановка задачи верификации. Ключевые слова: программа, модель программы, модель вычисления, синтаксис и семантика программы, задача верификации.
