Information Technology Reference
In-Depth Information
chosen in the design determine the nature of the elementary computations that can be
performed locally by the components, the emphasis in the language is put on the co-
ordination mechanisms between system components rather than data refinement,
which focuses on computational aspects. As a result, CommUnity does not support
polymorphism directly.
In the above example, V is the set of channels in the design P. Each channel v is
typed with a sort from S. in(V) represents input channels, which read data from the
environment of the component and the component has no control over them. out(V)
and prv(V) are output channels and private channels, respectively. They are controlled
locally by the component. Output channels allow the environment to read data pro-
duced by the component, while private channels support internal activity that does not
involve the environment. We use loc(V) to represent out(V)
prv(V). The formula I
constrains potential initial states of the corresponding program. I is a formula in first-
order logic over the channels of the design.
For any action g, D(g) is a subset of loc(V) consisting of the local channels that can
be written to by action g (we call it the write frame of g). U(g) is a progress condition,
which establishes the upper bound for enabledness and L(g) indicates the lower
bound. In a program, L(g) = U(g), so the guards in a design define the “interval”
within which the guard of the action in a program implementing the design must lie.
R(g) is a condition on V and D(g)', where by D(g)' we mean the set of primed chan-
nels from D(g). Primed channels account for references to the values of channels after
the execution of an action. The condition is a first-order logic formula built from V
and D(g)'. Usually, we define it as a conjunction of implications of the form pre ⇒
post, which corresponds to a pre/post condition specification in the sense of Hoare
and where pre does not contain primed channels. Using this form, the number of con-
juncts in the formula will correspond to the number of channels in the write frame of
g, so that we can understand the meaning of the action fairly easily. Moreover, it will
be convenient for us to calculate the colimit of the diagram if we have put all the
designs in this form.
In order to study the relationship between designs, we need the formal definition
for designs as follows:
Definition 1. A design signature is a tuple (V,
Γ
, tv, ta, D) where:
V is the set of channels , which is an S-indexed family of mutually disjoint
sets. The channel is typed with sorts in S, which is a fixed set of data types
specified as usual via a first-order specification.
Γ
is a finite set of actions.
tv is a total function from V to {prv, in, out}, which partitions V into three
disjoint sets of channels, namely private, input and output channels, respec-
tively. Loc(V) represents the union of private and output channels.
ta is a total function from
into private and
shared actions. Only shared actions can serve as the synchronization points
with other designs.
Γ
to {sh, prv}, which divides
Γ
to 2 loc(V) . The write frame of action g is repre-
D is total function from
Γ
sented by D(g).
Search WWH ::




Custom Search