Information Technology Reference
In-Depth Information
Definition 4 (Composability of I/O-Signatures).
Two I/O-signatures
Σ
S
=(
V
S
,
O
S
)
and
Σ
T
=(
V
T
,
O
T
)
are
composable
if
V
prov
S
∩V
req
T
V
prov
T
∩V
req
S
1.
V
S
∩V
T
=(
)
∪
(
)
,
O
prov
S
∩O
req
T
O
prov
T
∩O
req
S
2.
O
S
∩O
T
=(
)
∪
(
)
.
The set
V
S
∩V
T
of
shared state variables
will be denoted by sh
(
V
S
,
V
T
)
and the
set
O
S
∩O
T
of
shared operations
will be denoted by sh
(
O
S
,
O
T
)
.
When two composable I/O-signatures are actually composed, the shared state
variables become internal. Likewise, the shared operations become internal rep-
resenting the synchronization of provided and required operations.
Definition 5 (Composition of I/O-Signatures).
The composition of two
composable I/O-signatures
Σ
S
=(
V
S
,
O
S
)
and
Σ
T
=(
V
T
,
O
T
)
is the I/O-
signature
Σ
S
⊗
Σ
T
=(
V
S
⊗V
T
,
O
S
⊗O
T
)
where
V
prov
S
V
prov
T
V
S
⊗V
T
)
prov
(
=(
)
\
sh
(
V
S
,
V
T
)
,
V
req
S
V
req
T
V
S
⊗V
T
)
req
(
=(
)
\
sh
(
V
S
,
V
T
)
,
V
S
⊗V
T
)
int
V
int
S
V
int
T
(
=
sh
(
V
S
,
V
T
)
,
O
prov
S
O
prov
T
O
S
⊗O
T
)
prov
=(
(
)
\
sh
(
O
S
,
O
T
)
,
O
req
S
O
req
T
O
S
⊗O
T
)
req
=(
(
)
\
sh
(
O
S
,
O
T
)
,
O
S
⊗O
T
)
int
=
O
int
S
O
int
T
(
sh
(
O
S
,
O
T
)
.
Two MIODs are composable if their signatures are composable and if the labels
occurring on their transitions satisfy certain syntactic constraints. Condition 1 in
Def. 6 is technically necessary to ensure that the composition of MIODs defined
below is well-formed. For instance, condition 1(a) requires that preconditions of
non-shared, provided operations must not include shared state variables; other-
wise the precondition of a provided operation in the composition would involve
internal state variables which is not allowed. Condition 2 in Def. 6 is needed from
an intuitive point of view. For instance, condition 2(a) requires that for shared,
provided operations preconditions of one MIOD can only talk about provided
variables which are known from the other MIOD as required variables.
Definition 6 (Composability of MIODs).
Two MIODs
S
and
T
are
com-
posable
if their signatures
Σ
S
=(
V
S
,
O
S
)
and
Σ
T
=(
V
T
,
O
T
)
are composable,
Δ
may
S
if for all transitions
(
s,
[
ϕ
S
]
op
[
π
S
]
,s
)
∈
we have
1. if op
/
∈
sh
(
O
S
,
O
T
)
then
∈O
prov
S
V
prov
S
(a) if op
then
ϕ
S
∈S
(
\
sh
(
V
S
,
V
T
)
,par
(
op
))
,
∈O
req
S
V
req
S
(b) if op
then
π
S
∈T
(
\
sh
(
V
S
,
V
T
)
,par
(
op
))
,
2. if op
∈
sh
(
O
S
,
O
T
)
then
∈O
prov
S
V
prov
S
∩V
re
T
,par
(
op
))
,
then
ϕ
S
∈S
(a) if op
(
∈O
req
S
V
req
S
∩V
prov
T
(b) if op
then
π
S
∈T
(
,par
(
op
))
,
Δ
may
T
and if the same holds symmetrically for all transitions
(
t,
[
ϕ
T
]
op
[
π
T
]
,t
)
∈
.
Search WWH ::
Custom Search