Information Technology Reference
In-Depth Information
condition enforces the preservation of the type of each attribute by the morphism.
Output and private attributes of the component should keep their classification in the
system, while input attributes may be turned into output attributes, when they are
synchronized with output channels of other components and thus represented as out-
put channels of the system. The restriction over action domains means that the type of
each action is preserved by the morphism. In other words, the images of the write
frame of an action in the source program must be contained in the write frame of the
corresponding action in the target program. Notice that more attributes may be in-
cluded in the domain of the target program's action via a morphism. This is intuitive
because an action of a component may be shared with other components within a
system and, hence, has a larger domain.
Signature morphisms provide us with the means for relating a design with its su-
perpositions. However, superposition is more than just a relationship between signa-
tures on the level of syntax. To capture its semantics, we need a way of relating the
models of the two designs as well as the terms and propositions that are used to build
them.
Signature morphisms define translations between the languages associated with
each signature in the obvious way:
Definition 11.
Given a signature morphism
σ
:
θ
1
→
θ
2
, we can define translations
between the languages associated with each signature:
•
if t is a term:
σ
(t) ::=
(a) if t is a variable a
c if t is a constant c
f(
σ
σ
(t
1
),…,
σ
(t
n
)) if t= f(t
1
,…, t
n
)
•
if
φ
is a proposition:
σ
(
φ
) ::=
σ
(t
1
) =
σ
(t
2
) if
φ
is t
1
= t
2
σ
(t
1
) p
s
σ
(t
2
) if
φ
is t
1
p
s
t
2
σ
(
φ
1
) ⇒
σ
(
φ
2
) if
φ
is
φ
1
⇒
φ
2
σ
(
φ
1
)
∧
σ
(
φ
2
) if
φ
is
φ
1
∧
φ
2
'
¬σ
(
φ
') if
φ
is
¬φ
Definition 12.
Given a signature morphism
σ
:
θ
1
→
θ
2
and a
θ
2
-interpretation struc-
ture
S
=
(
T
,
A
,
G
), its
σ
-reduct, S
|
σ
, is the
θ
1
-interpretation structure (
T
,
A
|
σ
,
G
|
σ
),
-1
(g)).
That is, we take the same transition system of the target design and interpret attrib-
ute symbols of the source design in the same way as their images under
where
A
|
σ
(a) =
A
(
σ
(a)),
G
|
σ
(g) =
∪
G
(
σ
σ
, and action
-1
. Reducts provide
us with the means for relating the behavior of a design with that of the superposed
one. The following proposition establishes that properties of reducts are characterized
by translation of properties.
symbols of the source design as the union of their images under
σ
Proposition 1.
Given a
θ
1
proposition
φ
and a
θ
2
-interpretation structure S=(
T, A, G
),
.
Superposition morphisms that preserve locality are called
regulative
superposition
morphisms and are defined as follows:
we have for every w
∈
W
: (
S
, w)
t
σ
(
φ
) iff (
S
|
σ
, w)
t
φ
Search WWH ::
Custom Search