In 1958 A.A. Lyapunov and Yu. I. Yanov gave rise to a new branch of computer science – theory of program schemata. Initially, this theory deals only with program schemata that were called then as Yanov schemata. Later some other variants of formal models of programs were developed. One of such variants is a theory of model of recursive programs. Model of recursive programs is a suitable abstraction for the analysis of sequential programs augmented with procedures. In this paper we define formally models of recursive programs and present some recent results on studying the key problems of this theory. First, we show that a subclass of smooth models of recursive programs with an approximation relation forms upper semi-lattice. Next we demonstrate can be decidable as well as undecidable in some models of recursive programs. Then we select a specific class of models (gateway models) which is the most perspective for further research and outline techniques which may be used for designing equivalence checking procedures. Finally, we present systems of equivalent transformations and show that they are complete in some models of recursive programs.

model of programs, recursive program, approximation relation, equivalence checking problem, decision procedure, equivalent transformation

Mathematical problems and theory of numerical methods