4189
правок
Program schemata: различия между версиями
Материал из WEGA
нет описания правки
Glk (обсуждение | вклад) (Новая страница: «'''Program schemata''' --- схемы программ.») |
Glk (обсуждение | вклад) Нет описания правки |
||
| Строка 1: | Строка 1: | ||
'''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>\alpha</math> describes ('''models''') a set <math>P_\alpha</math> of concrete programs, and two program schemata <math>\alpha</math> and <math>\beta</math> | |||
are considered as '''functionally equivalent''' only if any concrete programs <math>p_1\in P_\alpha</math> and <math>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>\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>S_1</math> and <math>S_2</math> are '''equivalent''' in the sense of the history <math>H</math>, if for any interpretation <math>I\in \Omega</math> concrete programs obtained from <math>S_1</math> and <math>S_2</math> are equivalent in the sense of this history. | |||
