Large-block schema

Материал из WikiGrapp
Перейти к:навигация, поиск

Large-block schema --- крупноблочная схема.

Large-block schema is an abstract model of imperative programs that is based on the notion of a program as a finite set of structured statements processing a finite set of structured variables. The class of large-block schemata includes (as proper subslasses) other models of imperative programs such as Martynyuk schemata and standard program schemata. It is complete with respect to simulation and allows the program optimizations affecting both program memory and control structure to be investigated.

Let \Sigma be an alphabet which consists of mutually disjoint sets of variables (denoted by X), constants, operator symbols, predicate symbols, access symbols and k-case symbols for any integer k > 1.

A large-block program schema \alpha is a triple (G_\alpha, R_\alpha, \Omega_\alpha), where G_\alpha is a flow-diagram, R_\alpha is a coloring and \Omega_\alpha is a nonempty set of interpretations.

A flow-diagram (or control-flow graph) G_\alpha is an ordered directed graph whose nodes are instructions (or statements). It has exactly one START instruction and a nonempty set of STOP instructions. An instruction with k outgoing arcs is called a krecognizer (or recognizer) if k > 1 and a transformer if k=1.

Every instruction S has a set of operands (divided into four disjoint subsets: strong inputs, nonstrong inputs, strong outputs, nonstrong outputs); the set for the START instruction is empty, and the set for each STOP consists of only nonstrong inputs. There are two relations on the set of operands: an equivalence relation which divides the set into subsets of (informationally) connected operands and a symmetric relation which consists of pairs of so called (informationally) incompatible operands. It is assumed that there is no such pairs of operands which are both connected and incompatible, and the outputs of every instruction are mutually incompatible.

Let S be a statement of G_\alpha distinct from START and STOP. Every output d of S has a data term \Phi of S; \Phi is built up using the inputs of S and the constants, and applying the operation symbols to them. If d is a nonstrong output of S and has \Phi, d has also an access term of the form g(\Phi_1,\Phi_2,\ldots,\Phi_n, \Phi, d), where g is an (n+2)-ary access symbol and \Phi_1,\Phi_2,\ldots,\Phi_n are data terms of S. S can have a predicate term being a predicate symbol applied to data terms of S, all inputs of which are strong ones. If S is a k-recognizer, S has a kcase term being a k-case symbol applied to data terms of S.

The colouring R_\alpha is such a mapping of the set of all operands on some subset X_\alpha (called the memory of the schema \alpha) of X that R_\alpha(a)=R_\alpha(b) for any two connected operands and R_\alpha(a)\neq R_\alpha(b) for any two incompatible operands. If d is a strong or nonstrong input (output, respectively) of a statement S, then x=R_\alpha(d) is called a strong or nonstrong argument (result, respectively) of S.

An interpretaion I\in \Omega_\alpha consists of

(1) a nonempty set D_\alpha called the domain of I;

(2) an assignment of an element I(c)\in D_I to each variable and constant c;

(3) an assignment of a function I(f): D_I^n  \rightarrow D_I to every n-ary operator symbol f;

(4) an assignment of a predicate I(h): D_I^n  \rightarrow \{ true, false\} to every n-ary predicate symbol h;

(5) an assignment of a (access) function I(g): D_I^n  \rightarrow D_I to every n-ary access symbols g, such that for any access functions F_1, F_2, \ldots, F_m and for any elements a_1^1, \ldots,  a_{k_1-1}^1, a_1^2, \ldots, a_{k_1-1}^2, \ldots,  a_1^m,\ldots, a_{k_1-1}^m, a from D_I if F_1=F_m, a_1^1=a_1^m, \ldots a_{k-1}^1=a_{k_m-1}^m, then F_1( a_1^1, \ldots,  a_{k_1-1}^1, F_2( a_1^2, \ldots, a_{k_1-1}^2, \ldots, F_{m-1}(  a^{m-1}_1, \ldots,  a_{k_1-1}^{m-1}, F_m(  a_1^m,\ldots, a_{k_1-1}^m, a))\ldots))= F_1( a_1^1, \ldots,  a_{k_1-1}^1, F_2( a_1^2, \ldots, a_{k_1-1}^2, \ldots, F_{m-1}(  a^{m-1}_1, \ldots,  a_{k_1-1}^{m-1},a)  \ldots));

(6) an assignment of a function I(T): D_I^n  \rightarrow \{1,2,\ldots, k\} to every n-ary k-case symbol T.

Inclusion and equivalence of schemata are defined as follows:

(1) \alpha includes (or extends) \beta iff \Omega_\alpha \subseteq\Omega_\beta and for any I\in \Omega_\alpha, val(\alpha, I)=val(\beta, I) whenever val(\alpha, I) (see Value of schema under interpretation) is defined;

(2) \alpha and \beta are (strongly) equivalent iff either of them includes the other.