Database Reference
In-Depth Information
where:
1.
S
M
is a set of memory-states;
2.
Oper
is a set of operators (functions)
f
:
S
M
→
S
M
(i.e., the elementary opera-
tions of machine);
3.
Te s t
is a set of test-functions
f
:
S
M
→{
0
,
1
}
;
4.
In
M
is an initial input-function
In
M
:
INP
0
→
S
M
, where
INP
0
is a set of all
initial input-values;
5.
In
E
is a (partial) input function
In
E
:
INP
×
S
M
→
S
M
, where
INP
is a set of all
input values
z
i
∈
INP,z
i
={
z
i
1
,z
i
2
,...,z
ik
}
,k
≥
1;
6.
Out
M
is an output function
Out
M
:
S
M
→
OUT
, where
OUT
is a set of all output
values.
Oper
is the subset of operators of a relational
algebra used as a database-sublanguage, to manipulate the data in relational form.
Notice that in our case
Σ
RE
⊂
Definition 36
A program P for an input-extended machine
MI
is a finite set of
instructions, where any two different instructions have two different addresses. Each
instruction has one of the following syntax forms:
1. A triple
(i,f,j)
where
i
is its address,
j
is the address of the next instruction and
f
In
∗
E
}
, where
In
∗
E
:
∈
Oper
∪{
INP
×
S
M
→
S
M
is a total function defined for
∈
×
any
(z, st)
INP
SM
by:
In
∗
E
(z, st)
=
In
E
(z, st)
if
(z, st)
is an element of the domain of
In
E
;
st,
otherwise
.
∈
2. A quadruple
(i,t,j,k)
where
i
is its address,
t
Te s t
,
j
is the address of the next
instruction when
t
returns 1, while
k
is the address of the next instruction when
t
returns 0.
3. The initial instruction of a program has the address 0. Every next address, which
appears in a program P, such that it is not an address of some instruction in P, is
an address of the final state of P.
In order to define this operational effect of the execution of a program P on a
machine
MI
, we use the following
Computation System
:
Definition 37
An
execution of a program
P on a machine
MI
is a Computation
System
CS
=
(TrS, In
S
, Out
S
, Stop
S
)
as follows:
1.
TrS
→
P
)
is a deterministic transition system where
S
P
=
(i, st)
=
(S
P
,
|
i
is the address of some instruction of P
,
S
M
is the state of
M
before execution of this
i
th instruction
st
∈
is a set of configurations, and
→
P
is a function defined for any
(i, st)
by
(i, st),
j,λIn
∗
E
(z)(st)
∈→
P
if
i, In
∗
E
,j
∈→
P
,