Formal model of programs is defined as a set of interpretations that specify program runs. A program scheme is called free if every syntactically admissible trace in the scheme is traversable by a run in some interpretation of this model. A free scheme is called completely free if every transition from one program instruction to another is supplied with checking of all logical conditions occurred in the scheme. A formal model satisfies a (Completely) Free Scheme Requirement if every program scheme has an equivalent in this model (completely) free scheme. It is shown that Completely Free Scheme Requirement is not equally matched Free Scheme Requirement. We define some operations on formal models of programs to add new program statements and logical conditions. A number of necessary and sufficient conditions for Completely Free Scheme Requirement are specified in terms of these operations. It is also shown that the class of regular formal models whose interpretations are defined by finite state automata is in a some sense the minimal class of formal models of programs which satisfies Completely Free Scheme Requirement.

formal model of programs, program scheme, free scheme, completely free scheme, finite state automaton

Mathematical problems and theory of numerical methods