Information Technology Reference
In-Depth Information
N' registers for all futures in v
[
f,v, itf
]
N
0
[This.itf,N'.itf']
∈
bindings
[
f
,v,itf
]
itf
itf'
N'
[ f',v,itf' ]
fresh f'
FRL
[
f
→ N
0
]
f'=f
Results
Fig. 3.
CommChild rule
CommChild
:
Cqueue s= R#Q;
src=This(invkItf R), dest=N'.i2
∈
bindings;
f'
∈
set (RqIdList S) ; subCp^N' = Some C'
=
⇒
S
Composite N itf sub b s
→
R
Composite N itf
(sub<-(C'
←
id=f', parameter=(parameter R),invokedItf=i2
)) b
(s
Cqueue:=Q,CcomputedResults:=CcomputedResults s @
[
fid=id R,fValue=(0,[f'])
]
),
(f,N)#(map (
λ
id.(id,N')) (snd(parameter R)))
The rule expresses request delegation between a composite component
N
and one
N
.Therequest
R
f, v,
of its subcomponents
(shown as its constituents [
itf
]in
N
Figure 3) that has been sent to the parent
is dequeued from its request queue.
Anewfuture
f
is created and added to the result list (
CcomputedResults
)of
the parent as the result for this request
R
. A new request (shown as its con-
stituents [
f
,v,
itf
]) is enqueued in the subcomponent
N
. In the Isabelle code
snippet, we use the shortcut notation
for the enqueue operation. The target
subcomponent is determined using the bindings: if
This
←
N
.
itf
.
itf
is bound to
then the request is sent to the interface
itf
of the subcomponent
N
,where
itf
is the external interface of
by which the request had arrived before. Note the
use of the getCp primitive:
subCp^N'=Some C'
ensures that subcomponent of
name
N'
exists and is
C'
.Alsothe
changeCp
primitive (
<-
) is quite useful here
to update the subcomponent by enqueueing a new request to it.
Let us conclude this section by showing a property we proved in our framework
that deals with component semantics. The following lemma shows that the set
of names of components inside a component is unchanged by reduction.
N
lemma
red_names_eq:
S
c1
→
R
c2, RL; CorrectComponentWeak c1
=
⇒
getName ' (cpSet c2) = getName '(cpSet c1)
The proof is approximately 60 lines long, it is done by analysis on the reduction
rule. It relies on a few lemmas relating names with reduction rules, and on most
of the lemmas presented in Section 3. A crucial auxiliary lemma is the following
one that is purely structural and unrelated with our semantics.
