Program schemata

Program schemata --- схемы программ.

Program schemata are a class of abstract programs with an equivalence relation between them. They retain many structural properties of programs, in particular, splitting into statements with indications of the information and control flow between them. This makes it possible for program schemata to construct many of the characteristics typical for concrete programs, for example, histories of program execution. In program schemata, variables, operations and predicates are represented by formal symbols without any internal properties. These formal objects keep only the information needed for const\-ruc\-ting histories of their realizations, for example, for formal operations, only the number of formal arguments and the names of formal variables substituted for them are indicated; for a formal statement of control transfer, only those statements to which control may be transferred are labelled, and so on.

Every program scheme [math]\displaystyle{ \alpha }[/math] describes (models) a set [math]\displaystyle{ P_\alpha }[/math] of concrete programs, and two program schemata [math]\displaystyle{ \alpha }[/math] and [math]\displaystyle{ \beta }[/math] are considered as functionally equivalent only if any concrete programs [math]\displaystyle{ p_1\in P_\alpha }[/math] and [math]\displaystyle{ p_2\in P_\beta }[/math] having the same structure are functionally equivalent (i.e. computes the same function).

Concrete programs can be obtained from schemata by means of interpretation which consists in bringing some concrete variables and operations into correspondence with formal variables and operations. Very important is the concept of the set [math]\displaystyle{ \Omega }[/math] of all interpretations of program schemata. The theory is developed in such a way that a fact ascertained for some schema should be true for any interpreting program. In particular, in this way the notion of equivalence of two program schemata is introduced: two program schemata [math]\displaystyle{ S_1 }[/math] and [math]\displaystyle{ S_2 }[/math] are equivalent in the sense of the history [math]\displaystyle{ H }[/math], if for any interpretation [math]\displaystyle{ I\in \Omega }[/math] concrete programs obtained from [math]\displaystyle{ S_1 }[/math] and [math]\displaystyle{ S_2 }[/math] are equivalent in the sense of this history.