Information Technology Reference
In-Depth Information
Of course, un-binding does not maintain completeness, and this can be proved
in our framework.
lemma
unbinding_incomplete:
b
∈
bindings; CorrectComponentStructure (Composite N itf sub bindings s)
=
⇒¬
Complete (unbind (Composite N itf sub bindings s) b)
This lemma is proved in only 35 lines of simple Isabelle/HOL code, thanks to
the properties presented in Section 3.5. The proof can be sketched as follows.
CorrectComponentStructure
imposes that in bindings
src b
is connected only
once, thus, in
bindings-
{
b
}
,
src b
is not connected anymore. Now,
src b
can
be either
This N
if
b
connects an internal client interface to a sub-component,
or of the form
CN.N
if it connects a sub-component to another interface. In the
first case, the new component does not ensure
allInternalItfsBound
anymore,
and in the second case, it is
allExternalItfsBound
that is not true for the
component with name
CN
;notethat
CorrectComponentStructure
ensures the
existence of such a component.
Component replacement.
Let us now introduce a reconfiguration primitive that
would automatically maintain completeness.
primrec
Replace:: Component
⇒
Name
⇒
Component
⇒
Component
where
Replace (Primitive N itf s) N1 C = (Primitive N itf s) |
Replace (Composite N itf sub binds s) N1 C = addSubCp (removeSubCp
(Composite N itf sub ((
λ
b.RenameBinding b N1 (getName C))'binds) s) N1) C
This primitive maintains completeness of a correct component as expressed in
the following lemma:
lemma
replace_complete:
sub^(getName C')=None; sub^N'=Some oldC; getItfs oldC=getItfs C';
Complete C'; Complete (Composite N itf sub bindings s);
CorrectComponentStructure C';
CorrectComponentStructure (Composite N itf sub bindings s)
=
⇒
Complete (Replace (Composite N itf sub bindings s) N' C')
This lemma requires that all involved original components are correct and com-
plete, that the replaced component is in the composition, but not the replace-
ment one, and that those two components have the same interfaces. A similar
lemma proving
CorrectComponentStructure
for the result of the replacement
operation is also proved.
Of course, the replace primitive can be expressed by lower level reconfiguration
operations, i.e. an unbind, remove, add, bind sequence. A lemma equivalent to
the preceding one could also be proved. Such a lemma would be more general
but a little more complex to express because it would need to relate the set of
unbound bindings, the set of re-bound ones, and the component involved in the
add-remove operations.
