Information Technology Reference
In-Depth Information
26. Stein, D., Hanenberg, S., Unland, R.: Expressing different conceptual models of join
point selection in aspect-oriented design. In: Proceedings of AOSD 2006 (2006)
27. TopCaseD, (2006), http://www.topcased.org/
28. Walker, R.J., Viggers, K.: Implementing protocols via declarative event patterns.
In: ACM Sigsoft International Symposium on Foundations of Software Engineering
(FSE-12). 29(6), 159-169, (2004)
29. Whittle, J., Araujo, J.: Scenario modelling with aspects. IEE Proceedings - Soft-
ware 151(4), 157-172 (2004)
Appendix
This appendix contains the proof of Theorem 1.
Proof:
To demonstrate Theorem 1, we assume that two overtaking messages cannot
have the same name and we use the following lemma which can be found in the
book “ Introduction to Lattices and Order ” [9](p.110):
Lemma 1. Let (
L, ∨, ∧
) be a triple where
L
is a non-empty set equipped with
two binary operations
and
which satisfy for all
a, b, c ∈ L
:
(1)
a ∨ a
=
a
and
a ∧ a
=
a
(idempotency laws);
(2)
a ∨ b
=
b ∨ a
and
a ∧ b
=
b ∧ a
(commutative laws );
(3) (
a ∨ b
)
∨ c
=
a ∨
(
b ∨ c
) et (
a ∧ b
)
∧ c
=
a ∧
(
b ∧ c
) (associative laws);
(4)
a ∨
(
a ∧ b
)=
a
et
a ∧
(
a ∨ b
)=
a
(absorption laws).
then:
;
( ii ) If we define ≤ by a ≤ b if a ∨ b = b,then≤ is an order relation;
(
(
i
)
∀a, b ∈ L, a ∨ b
=
b ⇔ a ∧ b
=
a
iii
) With
as in (
ii
) , (
L, ≤
) is a lattice such that
∀a, b ∈ L, a ∨ b
sup{a, b}
=
and a ∧ b = inf{a, b}.
We will show that
J P,M canbeequippedwithtwobinaryoperations
and
which verify the properties 1-4 of the lemma.
Let
J P,M be the set of join points corresponding to a pointcut
P
=(
I P ,E P ,
P ,A P P P , ≺ P ) in a bSD
M
=(
I,E,≤,A,α,φ,≺
). Let
and
be the
operators defined for each
J i ,
J j of
J P,M by:
{e, f ∈ J i |e ≺ f, ∃e ∈ E P ,e
e )
e )
J i ∨ J j =
=
μ i 1 (
j 1 (
≤ e}∪
{e, f ∈ J j |e ≺ f, ∃e ∈ E P ,e
e )
e )
=
μ j 1 (
i 1 (
≤ e}
{e, f ∈ J i |e ≺ f, ∃e ∈ E P ,e
e )
e )
J i ∧ J j =
=
μ i 1 (
,e ≤ μ j 1 (
}∪
{e, f ∈ J j |e ≺ f, ∃e ∈ E P ,e
e )
e )
=
μ j 1 (
,e ≤ μ i 1 (
}
μ i =
i 0 i 1 i 2
>
and
μ j =
j 0 j 1 j 2
>
being the isomorphisms
associating
P
to the respective join points
J i and
J j .
 
Search WWH ::




Custom Search