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 be an alphabet which consists of mutually disjoint sets of variables (denoted by ), constants, operator symbols, predicate symbols, access symbols and -case symbols for any integer .
A large-block program schema is a triple , where is a flow-diagram, is a coloring and is a nonempty set of interpretations.
A flow-diagram (or control-flow graph) 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 outgoing arcs is called a recognizer (or recognizer) if and a transformer if .
Every instruction 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 be a statement of distinct from START and STOP. Every output of has a data term of ; is built up using the inputs of and the constants, and applying the operation symbols to them. If is a nonstrong output of and has , has also an access term of the form , where is an ()-ary access symbol and are data terms of . can have a predicate term being a predicate symbol applied to data terms of , all inputs of which are strong ones. If is a -recognizer, has a case term being a -case symbol applied to data terms of .
The colouring is such a mapping of the set of all operands on some subset (called the memory of the schema ) of that for any two connected operands and for any two incompatible operands. If is a strong or nonstrong input (output, respectively) of a statement , then is called a strong or nonstrong argument (result, respectively) of .
An interpretaion consists of
(1) a nonempty set called the domain of ;
(2) an assignment of an element to each variable and constant ;
(3) an assignment of a function to every -ary operator symbol ;
(4) an assignment of a predicate true, false to every -ary predicate symbol ;
(5) an assignment of a (access) function to every -ary access symbols , such that for any access functions and for any elements from if , then ;
(6) an assignment of a function to every -ary -case symbol .
Inclusion and equivalence of schemata are defined as follows:
(1) includes (or extends) iff and for any , whenever (see Value of schema under interpretation) is defined;
(2) and are (strongly) equivalent iff either of them includes the other.