Revision as of 21:53, 9 October 2006

This page shows

Example 1

The system

In this example we are studying a symple system with three classes that contains both renaming and selects:

class
   C1
feature
   f1 do ... end
   g1 do ... end
end

class
   C2
inherit
   B
      rename f1 as f2, g1 as g2 
      redefine f2, g2 end
feature
   f2 do ... end
   g2 do ... end
end

class
   C3
inherit
   C2
      select f1 end
   C1 
      redefine f1, g1 
      select g1 end
feature
   f1 do ... end
   g1 do ... end
end

This system is defined by:

$S = {C_{1}, C_{2}, C_{3}}$
$S_{1} = {C_{1}}, S_{2} = {C_{1}, C_{2}}, S_{3} = {C_{1}, C_{2}, C_{3}}$
$τ = {C_{1} \mapsto {f_{1} \mapsto \underline{C_{1} . f_{1}}, g_{1} \mapsto \underline{C_{1} . g_{1}}}, C_{2} \mapsto {f_{2} \mapsto \underline{C_{2} . f_{2}}, g_{2} \mapsto \underline{C_{2} . g_{2}}}, C_{3} \mapsto {f_{1} \mapsto \underline{C_{3} . f_{1}}, g_{1} \mapsto \underline{C_{3} . g_{1}}}}$
$η = {C_{2} \mapsto {C_{1} \mapsto {f_{1} \mapsto f_{2}, g_{1} \mapsto g_{2}}}}$
$α = {C_{2} \mapsto {C_{1}}, C_{3} \mapsto {C_{2}, C_{1}}}$
$σ = {C_{3} \mapsto {C_{2} \mapsto {f_{1}}, C_{2} \mapsto {g_{1}}}}$

The naming function

We proceed by calculating the naming function. According to its definition we have to do that incrementaly. Meaning that we first calculate $β_{S_{1}}$ then $β_{S_{2}}$ and finally $β_{S_{3}}$ .

Calculating $β_{S_{1}}$

Since $β_{S_{1}}$ contains only one class it is sufficient to define $β_{S_{1}} (C_{1} \mapsto C_{1})$ . According to the definition:

$β_{S_{1}} (C_{1} \mapsto C_{1}) = id (dom (τ_{1})) \cup UNION b \cdot (b \in α_{1} | id (ran (β_{S_{0}} (b \mapsto b) ≪ η_{1, b})))$

We can forget about the right part of the union since $C_{1}$ has no base classes. So we need to calculate: $id (dom (τ_{1}))$ .

This done we calculate:

$τ_{1} = τ (C_{1}) = {f_{1} \mapsto \underline{C_{1} . f_{1}}, g_{1} \mapsto \underline{C_{1} . g_{1}}}$
$dom (τ_{1}) = {f_{1}, g_{1}}$
$id (dom (τ_{1})) = {f_{1} \mapsto f_{1}, g_{1} \mapsto g_{1}}$

So we get:

$β_{S_{1}} (C_{1} \mapsto C_{1}) = {f_{1} \mapsto f_{1}, g_{1} \mapsto g_{1}}$

Calculating $β_{S_{2}}$

We show the calculation of the different (four) parts of the function in separate sections:

Calculate $β_{S_{2}} (C_{1} \mapsto C_{1})$

According to the definition: $β_{S_{2}} (C_{1} \mapsto C_{1}) = β_{S_{1}} (C_{1} \mapsto C_{1}) = {f_{1} \mapsto f_{1}, g_{1} \mapsto g_{1}}$

Calculate $β_{S_{2}} (C_{2} \mapsto C_{1})$

According to the definition: $β_{S_{2}} (C_{2} \mapsto C_{1}) = \emptyset$

Calculate $β_{S_{2}} (C_{2} \mapsto C_{2})$

According to the definition: $β_{S_{2}} (C_{2} \mapsto C_{2}) = id (dom (τ_{2})) \cup UNION b \cdot (b \in α_{2} | id (ran (β_{S_{1}} (b \mapsto b) ≪ η_{2, b})))$

Lets calculate the left part first:

$τ_{2} = τ (C_{2}) = {f_{2} \mapsto \underline{C_{2} . f_{2}}, g_{2} \mapsto \underline{C_{2} . g_{2}}}$
$id (dom (τ_{2})) = {f_{2} \mapsto f_{2}, g_{2} \mapsto g_{2}}$

And now the right part:

$UNION b \cdot (b \in {C_{1}} | id (ran (β_{S_{1}} (b \mapsto b) ≪ η_{2, b}))) = id (ran (β_{S_{1}} (C_{1} \mapsto C_{1}) ≪ η_{2, C_{1}}))$
$β_{S_{1}} (C_{1} \mapsto C_{1}) = {f_{1} \mapsto f_{1}, g_{1} \mapsto g_{1}}$
$η_{2, C_{1}} = η (C_{2}) (C_{1}) = {f_{1} \mapsto f_{2}, g_{1} \mapsto g_{2}}$
${f_{1} \mapsto f_{1}, g_{1} \mapsto g_{1}} ≪ {f_{1} \mapsto f_{2}, g_{1} \mapsto g_{2}} = {f_{1} \mapsto f_{2}, g_{1} \mapsto g_{2}}$
$id (ran ({f_{1} \mapsto f_{2}, g_{1} \mapsto g_{2}})) = {f_{2} \mapsto f_{2}, g_{2} \mapsto g_{2}}$

So we get:

$β_{S_{2}} (C_{2} \mapsto C_{2}) = {f_{2} \mapsto f_{2}, g_{2} \mapsto g_{2}}$

Calculate $β_{S_{2}} (C_{1} \mapsto C_{2})$

According to the definition: $β_{S_{2}} (C_{1} \mapsto C_{2}) = {β_{S_{2}}}^{'} (C_{1} \mapsto C_{2}) ≪ θ_{S_{2}} (C_{1} \mapsto C_{2})$

Where: ${β_{S_{2}}}^{'} (C_{1} \mapsto C_{2}) = UNION b \cdot (b \in α_{2} | β_{S_{1}} (C_{1} \mapsto b); (id (ran (β_{S_{1}} (C_{1} \mapsto b))) ≪ η_{2, b}))$

And: $θ_{S_{2}} (C_{1} \mapsto C_{2}) = UNION b \cdot (b \in α_{2} | β_{S_{1}} (C_{1} \mapsto b); (id (ran (β_{S_{1}} (C_{1} \mapsto b))) ≪ η_{2, b}) ▹ σ_{2, b})$

Here are the steps taken to compute the part:

βS1(C1↦C1);(id(ran(βS1(C1↦C1)))≪η2,C1)
1. $id (ran (β_{S_{1}} (C_{1} \mapsto C_{1}))) = {f_{1} \mapsto f_{1}, g_{1} \mapsto g_{1}}$
2. ${f_{1} \mapsto f_{1}, g_{1} \mapsto g_{1}} ≪ {f_{1} \mapsto f_{2}, g_{1} \mapsto g_{2}} = {f_{1} \mapsto f_{2}, g_{1} \mapsto g_{2}}$
3. ${f_{1} \mapsto f_{1}, g_{1} \mapsto g_{1}}; {f_{1} \mapsto f_{2}, g_{1} \mapsto g_{2}} = {f_{1} \mapsto f_{2}, g_{1} \mapsto g_{2}}$
4. ${β_{S_{2}}}^{'} (C_{1} \mapsto C_{2}) = {f_{1} \mapsto f_{2}, g_{1} \mapsto g_{2}}$
βS1(C1↦C1);(id(ran(βS1(C1↦C1)))≪η2,C1)▹σ2,C1
1. $σ_{2, C_{1}} = \emptyset$
2. $id (ran (β_{S_{1}} (C_{1} \mapsto C_{1}))) ≪ \emptyset = \emptyset$
3. $β_{S_{1}} (C_{1} \mapsto C_{1}); \emptyset = \emptyset$
4. $θ_{S_{2}} (C_{1} \mapsto C_{2}) = \emptyset$
${f_{1} \mapsto f_{2}, g_{1} \mapsto g_{2}} ≪ \emptyset = {f_{1} \mapsto f_{2}, g_{1} \mapsto g_{2}}$

So:

$β_{S_{2}} (C_{1} \mapsto C_{2}) = {f_{1} \mapsto f_{2}, g_{1} \mapsto g_{2}}$

Putting the parts together:

We can know show the complete total function:

$β_{S_{2}} = {$	$(C_{1} \mapsto C_{1}) \mapsto {f_{1} \mapsto f_{1}, g_{1} \mapsto g_{1}}$
	$(C_{1} \mapsto C_{2}) \mapsto {f_{1} \mapsto f_{2}, g_{1} \mapsto g_{2}},$
	$(C_{2} \mapsto C_{1}) \mapsto \emptyset,$
	$(C_{2} \mapsto C_{2}) \mapsto {f_{2} \mapsto f_{2}, g_{2} \mapsto g_{2}}}$

Calculating $β_{S_{3}}$

We will not show the complete construction of $β_{S_{3}}$ but restrict our self to the most interesting parts.

Calculate $β_{S_{3}} (C_{1} \mapsto C_{3})$

According to the definition: $β_{S_{3}} (C_{1} \mapsto C_{3}) = {β_{S_{3}}}^{'} (C_{1} \mapsto C_{3}) ≪ θ_{S_{3}} (C_{1} \mapsto C_{3})$

Where: ${β_{S_{3}}}^{'} (C_{1} \mapsto C_{3}) = UNION b \cdot (b \in α_{3} | β_{S_{2}} (C_{1} \mapsto b); (id (ran (β_{S_{2}} (C_{1} \mapsto b))) ≪ η_{3, b}))$

And: $θ_{S_{3}} (C_{1} \mapsto C_{3}) = UNION b \cdot (b \in α_{3} | β_{S_{2}} (C_{1} \mapsto b); (id (ran (β_{S_{2}} (C_{1} \mapsto b))) ≪ η_{3, b}) ▹ σ_{3, b})$

$β_{S_{2}} (C_{1} \mapsto C_{2}); (id (ran (β_{S_{2}} (C_{1} \mapsto C_{2}))) ≪ η_{3, C_{2}}) \cup β_{S_{2}} (C_{1} \mapsto C_{1}); (id (ran (β_{S_{2}} (C_{1} \mapsto C_{1}))) ≪ η_{3, C_{1}})$

@@ Line 337: / Line 337: @@
 ===Calculating <math>\beta_{S_3}</math>===
-We will not show the complete construction of <math>\beta_{S_3}</math> but restrict our self to the most interesting part:
+We will not show the complete construction of <math>\beta_{S_3}</math> but restrict our self to the most interesting parts.
-<math>\beta_{S_3}\left(C_1, C_3 \right)</math>
+====Calculate <math>\beta_{S_3} \left( C_1 \mapsto C_3 \right)</math>====
+According to the [[DynBindModel#The_naming_function|definition]]:
 <math>
 \beta_{S_3} \left( C_1 \mapsto C_3 \right)
@@ Line 348: / Line 349: @@
 </math>
+Where:
 <math>
 {\beta_{S_3}}^\prime \left( C_1 \mapsto C_3 \right)
@@ Line 363: / Line 365: @@
 \right)
 </math>
+And:
+<math>
+\theta_{S_3} \left( C_1 \mapsto C_3 \right)
+   =
+\mbox {UNION} \ b \ \cdot \ \left(
+   b \in \alpha_3
+      \ |\
+   \beta_{S_{2}} \left( C_1 \mapsto b \right)
+      ;
+   \left(
+      \mbox{id} \left( \mbox{ran} \left( \beta_{S_{2}} \left( C_1 \mapsto b \right) \right) \right)
+         \ll
+      \eta_{3,b}
+   \right)
+   \triangleright \sigma_{3,b}
+\right)
+</math>
 #<math>
     \beta_{S_{2}} \left( C_1 \mapsto C_2 \right)

DynBindModelExamples: Difference between revisions

Revision as of 21:53, 9 October 2006

Contents

Example 1

The system

The naming function

Calculating $β_{S_{1}}$

Calculating $β_{S_{2}}$

Calculate $β_{S_{2}} (C_{1} \mapsto C_{1})$

Calculate $β_{S_{2}} (C_{2} \mapsto C_{1})$

Calculate $β_{S_{2}} (C_{2} \mapsto C_{2})$

Calculate $β_{S_{2}} (C_{1} \mapsto C_{2})$

Putting the parts together:

Calculating $β_{S_{3}}$

Calculate $β_{S_{3}} (C_{1} \mapsto C_{3})$

Navigation menu

DynBindModelExamples: Difference between revisions

Revision as of 21:53, 9 October 2006

Example 1

The system

The naming function

Calculating βS1

Calculating βS2

Calculate βS2(C1↦C1)

Calculate βS2(C2↦C1)

Calculate βS2(C2↦C2)

Calculate βS2(C1↦C2)

Putting the parts together:

Calculating βS3

Calculate βS3(C1↦C3)

Navigation menu

Search

Calculating $β_{S_{1}}$

Calculating $β_{S_{2}}$

Calculate $β_{S_{2}} (C_{1} \mapsto C_{1})$

Calculate $β_{S_{2}} (C_{2} \mapsto C_{1})$

Calculate $β_{S_{2}} (C_{2} \mapsto C_{2})$

Calculate $β_{S_{2}} (C_{1} \mapsto C_{2})$

Calculating $β_{S_{3}}$

Calculate $β_{S_{3}} (C_{1} \mapsto C_{3})$