DynBindModelExamples: Difference between revisions

Latest revision as of 10:11, 11 April 2007

Template:Article will be deleted Author: Matthias Konrad

The system

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

class
   A
feature
   f1 do ... end
   g1 do ... end
end

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

class
   D
inherit
 
   A
      redefine f1, g1 
      select g1 end
   B
      select f2 end
feature
   f1 do ... end
   g1 do ... end
end

This system is defined by:

$S = {A, B, D}$

$τ = {A \mapsto {f 1 \mapsto \underline{A . f 1}, g 1 \mapsto \underline{A . g 1}}, B \mapsto {f 2 \mapsto \underline{B . f 2}, g 2 \mapsto \underline{B . g 2}}, D \mapsto {f 1 \mapsto \underline{D . f 1}, g 1 \mapsto \underline{D . g 1}}}$

$α = {A \mapsto \emptyset, B \mapsto {A}, D \mapsto {A, B}}$

$η = {A \mapsto \emptyset, B \mapsto {A \mapsto {f_{1} \mapsto f_{2}, g_{1} \mapsto g_{2}}}, D \mapsto {A \mapsto \emptyset, B \mapsto \emptyset}}$

$σ = {A \mapsto \emptyset, B \mapsto {A \mapsto \emptyset}, D \mapsto {A \mapsto {g_{1}}, B \mapsto {f_{2}}}}$

$C = {1 \mapsto A, 2 \mapsto B, 3 \mapsto D}$

The naming function

We proceed by calculating the naming function. According to its definition we have to do that incrementally. 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}} (A \mapsto A)$ . According to the definition:

$β_{S_{1}} (C_{1} \mapsto C_{1}) = id (dom (τ_{1}) \cup UNION b \cdot (b \in α_{1} | 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))
1. $τ_{1} = τ (C_{1}) = {f_{1} \mapsto \underline{C_{1} . f_{1}}, g_{1} \mapsto \underline{C_{1} . g_{1}}}$
2. $dom (τ_{1}) = {f_{1}, g_{1}}$
3. $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}}$

And hence:

$β_{S_{1}} = {(C_{1} \mapsto C_{1}) \mapsto {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} | 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}}}$
$dom (τ_{2}) = {f_{2}, g_{2}}$

And now the right part:

$UNION b \cdot (b \in {C_{1}} | ran (β_{S_{1}} (b \mapsto b) ≪ η_{2, b})) = 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}}$
$ran ({f_{1} \mapsto f_{2}, g_{1} \mapsto g_{2}}) = {f_{2}, 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 we get:

$β_{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})$

Note that we can omit $η_{3, b}$ from the formulas since it is always empty.

βS2(C1↦C2);id(ran(βS2(C1↦C2))) ∪ βS2(C1↦C1);id(ran(βS2(C1↦C1)))
1. $β_{S_{2}} (C_{1} \mapsto C_{2}) = {f_{1} \mapsto f_{2}, g_{1} \mapsto g_{2}}$
2. $id (ran (β_{S_{2}} (C_{1} \mapsto C_{2}))) = {f_{2} \mapsto f_{2}, g_{2} \mapsto g_{2}}$
3. $β_{S_{2}} (C_{1} \mapsto C_{2}); id (ran (β_{S_{2}} (C_{1} \mapsto C_{2}))) = {f_{1} \mapsto f_{2}, g_{1} \mapsto g_{2}}$
4. $β_{S_{2}} (C_{1} \mapsto C_{1}) = {f_{1} \mapsto f_{1}, g_{1} \mapsto g_{1}}$
5. $id (ran (β_{S_{2}} (C_{1} \mapsto C_{1}))) = {f_{1} \mapsto f_{1}, g_{1} \mapsto g_{1}}$
6. $β_{S_{2}} (C_{1} \mapsto C_{1}); id (ran (β_{S_{2}} (C_{1} \mapsto C_{1}))) = {f_{1} \mapsto f_{1}, g_{1} \mapsto g_{1}}$
7. ${f_{1} \mapsto f_{2}, g_{1} \mapsto g_{2}} \cup {f_{1} \mapsto f_{1}, g_{1} \mapsto g_{1}} = {f_{1} \mapsto f_{1}, f_{1} \mapsto f_{2}, g_{1} \mapsto g_{1}, g_{1} \mapsto g_{2}}$
βS2(C1↦C2);id(ran(βS2(C1↦C2))) ▹ σ3,C2 ∪ βS2(C1↦C1);id(ran(βS2(C1↦C1))) ▹ σ3,C1
1. $σ_{3, C_{2}} = σ (C_{3}) (C_{2}) = {f_{2}}$
2. $σ_{3, C_{1}} = σ (C_{3}) (C_{1}) = {g_{1}}$
3. $β_{S_{2}} (C_{1} \mapsto C_{2}); id (ran (β_{S_{2}} (C_{1} \mapsto C_{2}))) ▹ σ_{3, C_{2}} = {f_{1} \mapsto f_{2}}$
4. $β_{S_{2}} (C_{1} \mapsto C_{1}); id (ran (β_{S_{2}} (C_{1} \mapsto C_{1}))) ▹ σ_{3, C_{1}} = {g_{1} \mapsto g_{1}}$
5. ${f_{1} \mapsto f_{2}} \cup {g_{1} \mapsto g_{1}} = {f_{1} \mapsto f_{2}, g_{1} \mapsto g_{1}}$
6. ${f_{1} \mapsto f_{1}, f_{1} \mapsto f_{2}, g_{1} \mapsto g_{1}, g_{1} \mapsto g_{2}} ≪ {f_{1} \mapsto f_{2}, g_{1} \mapsto g_{1}} = {f_{1} \mapsto f_{2}, g_{1} \mapsto g_{1}}$

So we get:

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

The complete naming function

$β_{S_{3}} = {$	$(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}},$
	$(C_{1} \mapsto C_{3}) \mapsto {f_{1} \mapsto f_{2}, g_{1} \mapsto g_{1}},$
	$(C_{2} \mapsto C_{3}) \mapsto {f_{2} \mapsto f_{2}, g_{2} \mapsto g_{2}},$
	$(C_{3} \mapsto C_{3}) \mapsto {f_{1} \mapsto f_{1}, g_{1} \mapsto g_{1}, f_{2} \mapsto f_{2}, g_{2} \mapsto g_{2}},$
	$(C_{3} \mapsto C_{1}) \mapsto \emptyset,$
	$(C_{3} \mapsto C_{2}) \mapsto \emptyset}$

The dynamic binding function

To calculate the dynamic binding function, we need to get $δ_{S_{3}}$ . We will again calculate it incrementally:

Calculating $δ_{S_{1}}$

According to the definition:

$δ_{S_{1}} (C_{1} \mapsto C_{1}) = β_{S} (C_{1} \mapsto C_{1}); ((UNION b \cdot (b \in α_{1} | {(β_{S} (b \mapsto b); η_{1, b})}^{- 1}; δ_{S_{0}} (b \mapsto b))) ≪ τ_{1})$

Since $α_{1}$ is empty this simplifies to: $δ_{S_{1}} (C_{1} \mapsto C_{1}) = β_{S} (C_{1} \mapsto C_{1}); τ_{1} = {f_{1} \mapsto f_{1}, g_{1} \mapsto g_{1}}; {f_{1} \mapsto \underline{C_{1} . f_{1}}, g_{1} \mapsto \underline{C_{1} . g_{1}}}$

So we get: $δ_{S_{1}} = {(C_{1} \mapsto C_{1}) \mapsto {f_{1} \mapsto \underline{C_{1} . f_{1}}, g_{1} \mapsto \underline{C_{1} . g_{1}}}}$

Calculating $δ_{S_{2}}$

Again we calculate the different 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 \underline{C_{1} . f_{1}}, g_{1} \mapsto \underline{C_{1} . g_{1}}}$

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

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

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

According to the definition:

$δ_{S_{2}} (C_{2} \mapsto C_{2}) = β_{S} (C_{2} \mapsto C_{2}); ((UNION b \cdot (b \in α_{2} | {(β_{S} (b \mapsto b); η_{2, b})}^{- 1}; δ_{S_{1}} (b \mapsto b))) ≪ τ_{2})$

UNIONb⋅(b∈{C1}|(βS(b↦b);η2,b)−1;δS1(b↦b))=(βS(C1↦C1);η2,C1)−1;δS1(C1↦C1)
1. $β_{S} (C_{1} \mapsto C_{1}); η_{2, C_{1}} = {f_{1} \mapsto f_{2}, g_{1} \mapsto g_{2}}$
2. ${(β_{S} (C_{1} \mapsto C_{1}); η_{2, C_{1}})}^{- 1} = {f_{2} \mapsto f_{1}, g_{2} \mapsto g_{1}}$
3. ${(β_{S} (C_{1} \mapsto C_{1}); η_{2, C_{1}})}^{- 1}; δ_{S_{1}} (C_{1} \mapsto C_{1}) = {f_{2} \mapsto \underline{C_{1} . f_{1}}, g_{2} \mapsto \underline{C_{1} . g_{1}}}$
$τ_{2} = τ (C_{2}) = {f_{2} \mapsto \underline{C_{2} . f_{2}}, g_{2} \mapsto \underline{C_{2} . g_{2}}}$
${f_{2} \mapsto \underline{C_{1} . f_{1}}, g_{2} \mapsto \underline{C_{1} . g_{1}}} ≪ {f_{2} \mapsto \underline{C_{2} . f_{2}}, g_{2} \mapsto \underline{C_{2} . g_{2}}} = {f_{2} \mapsto \underline{C_{2} . f_{2}}, g_{2} \mapsto \underline{C_{2} . g_{2}}}$

So we get: $δ_{S_{2}} (C_{2} \mapsto C_{2}) = {f_{2} \mapsto \underline{C_{2} . f_{2}}, g_{2} \mapsto \underline{C_{2} . g_{2}}}$

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

According to the definition:

$δ_{S_{2}} (C_{1} \mapsto C_{2}) = β_{S} (C_{1} \mapsto C_{2}); ((UNION b \cdot (b \in α_{2} | {(β_{S} (b \mapsto b); η_{2, b})}^{- 1}; δ_{S_{1}} (b \mapsto b))) ≪ τ_{2})$

At this stage it should be clear how to calculate this, so we just give the result:

$δ_{S_{2}} (C_{1} \mapsto C_{2}) = {f_{1} \mapsto \underline{C_{2} . f_{2}}, g_{1} \mapsto \underline{C_{2} . 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 \underline{C_{1} . f_{1}}, g_{1} \mapsto \underline{C_{1} . g_{1}}},$
	$(C_{1} \mapsto C_{2}) \mapsto {f_{1} \mapsto \underline{C_{2} . f_{2}}, g_{1} \mapsto \underline{C_{2} . g_{2}}},$
	$(C_{2} \mapsto C_{1}) \mapsto \emptyset,$
	$(C_{2} \mapsto C_{2}) \mapsto {f_{2} \mapsto \underline{C_{2} . f_{2}}, g_{2} \mapsto \underline{C_{2} . g_{2}}}}$

Calculating $δ_{S_{3}}$

There is nothing new for this calculation so we just present the result:

$δ_{S_{3}} = {$	$(C_{1} \mapsto C_{1}) \mapsto {f_{1} \mapsto \underline{C_{1} . f_{1}}, g_{1} \mapsto \underline{C_{1} . g_{1}}},$
	$(C_{1} \mapsto C_{2}) \mapsto {f_{1} \mapsto \underline{C_{2} . f_{2}}, g_{1} \mapsto \underline{C_{2} . g_{2}}},$
	$(C_{2} \mapsto C_{1}) \mapsto \emptyset,$
	$(C_{2} \mapsto C_{2}) \mapsto {f_{2} \mapsto \underline{C_{2} . f_{2}}, g_{2} \mapsto \underline{C_{2} . g_{2}}},$
	$(C_{1} \mapsto C_{3}) \mapsto {f_{1} \mapsto \underline{C_{2} . f_{2}}, g_{1} \mapsto \underline{C_{3} . g_{1}}},$
	$(C_{2} \mapsto C_{3}) \mapsto {f_{2} \mapsto \underline{C_{2} . f_{2}}, g_{2} \mapsto \underline{C_{2} . g_{2}}},$
	$(C_{3} \mapsto C_{3}) \mapsto {f_{1} \mapsto \underline{C_{3} . f_{1}}, g_{1} \mapsto \underline{C_{3} . g_{1}}, f_{2} \mapsto \underline{C_{2} . f_{2}}, g_{2} \mapsto \underline{C_{2} . g_{2}}},$
	$(C_{3} \mapsto C_{1}) \mapsto \emptyset,$
	$(C_{3} \mapsto C_{2}) \mapsto \emptyset}$

Deriving the dynamic binding function

The function is now given. We evaluate it at two interesting points:

$δ (C_{1} \mapsto f_{1}) = {C_{1} \mapsto \underline{C_{1} . f_{1}}, C_{2} \mapsto \underline{C_{2} . f_{2}}, C_{3} \mapsto \underline{C_{2} . f_{2}}}$

$δ (C_{1} \mapsto f_{g}) = {C_{1} \mapsto \underline{C_{1} . f_{g}}, C_{2} \mapsto \underline{C_{2} . g_{2}}, C_{3} \mapsto \underline{C_{2} . g_{1}}}$

DynBindModelExamples: Difference between revisions

Latest revision as of 10:11, 11 April 2007

Contents

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})$

The complete naming function

The dynamic binding 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}}$

Deriving the dynamic binding function

Navigation menu

@@ Line 1: / Line 1: @@
-Author: Matthias Konrad
+[[Category:ECMA]]
+{{Article will be deleted}}
+Author: Matthias Konrad[[Category:ECMA]]
 ==The system==
-In this example we are studying a symple system with three classes that contains both renaming and selects:
+In this example we are studying a simple system with three classes that contains both renaming and selects:
 {|border="0" cellpadding="2" cellspacing="0" align="center"
@@ Line 7: / Line 10: @@
 |<code>[eiffel, N]
 class
-    C1
+    A
 feature
     f1 do ... end
@@ Line 16: / Line 19: @@
 <code>[eiffel, N]
 class
-    C2
+    B
 inherit
-    B
+    A
        rename f1 as f2, g1 as g2
        redefine f2, g2 end
@@ Line 29: / Line 32: @@
 <code>[eiffel, N]
 class
-    C3
+    D
 inherit
-    C2
-      select f2 end
+    A
-    C1
        redefine f1, g1
        select g1 end
+   B
+      select f2 end
 feature
     f1 do ... end
@@ Line 43: / Line 47: @@
 |}
 This system is defined by:
-*<math>S = \left\{ C_1, C_2, C_3 \right\} </math>
-*<math>S_1 = \left\{ C_1\right\}, S_2 = \left\{ C_1, C_2\right\}, S_3 = \left\{ C_1, C_2, C_3 \right\}</math>
+<math>S=\left\{ A, B, D\right\}</math>
-*<math>\tau =
+<math>\tau =
 \left\{
-    C_1 \mapsto \left\{ f_1 \mapsto \underline{C_1.f_1}, g_1 \mapsto \underline{C_1.g_1} \right\},
+    A \mapsto \left\{ f1 \mapsto \underline{A.f1}, g1 \mapsto \underline{A.g1} \right\},
-    C_2 \mapsto \left\{ f_2 \mapsto \underline{C_2.f_2}, g_2 \mapsto \underline{C_2.g_2} \right\},
+    B \mapsto \left\{ f2 \mapsto \underline{B.f2}, g2 \mapsto \underline{B.g2} \right\},
-    C_3 \mapsto \left\{ f_1 \mapsto \underline{C_3.f_1}, g_1 \mapsto \underline{C_3.g_1} \right\}
+    D \mapsto \left\{ f1 \mapsto \underline{D.f1}, g1 \mapsto \underline{D.g1} \right\}
 \right\}
 </math>
-*<math>\eta =
+<math>\alpha = \left\{
+   A \mapsto \emptyset,
+   B \mapsto \left\{ A \right\},
+   D \mapsto \left\{ A, B \right\}
+\right\}
+</math>
+<math>\eta =
 \left\{
-    C_2 \mapsto \left\{
+    A \mapsto \emptyset,
-       C_1 \mapsto \left\{ f_1 \mapsto f_2, g_1 \mapsto g_2 \right\}
+   B \mapsto \left\{
+       A \mapsto \left\{ f_1 \mapsto f_2, g_1 \mapsto g_2 \right\}
+   \right\},
+   D \mapsto \left\{
+      A \mapsto \emptyset, B \mapsto \emptyset
     \right\}
 \right\}
 </math>
-*<math>\alpha = \left\{
-    C_2 \mapsto \left\{ C_1 \right\},
+<math>\sigma = \left\{
-    C_3 \mapsto \left\{ C_2, C_1 \right\}
+    A \mapsto \emptyset,
+   B \mapsto \left\{ A \mapsto \emptyset \right\},
+    D \mapsto \left\{ A \mapsto \left\{ g_1 \right\},
+                     B \mapsto \left\{ f_2 \right\} \right\}
 \right\}
 </math>
-*<math>\sigma = \left\{
-   C_3 \mapsto \left\{ C_2 \mapsto \left\{ f_2 \right\}, C_1 \mapsto \left\{ g_1 \right\} \right\}
+<math>
-\right\}
+   C = \left\{ 1 \mapsto A, 2 \mapsto B, 3 \mapsto D \right\}
 </math>
 ==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 <math>\beta_{S_1}</math> then  <math>\beta_{S_2}</math> and finally <math>\beta_{S_3}</math>.
+We proceed by calculating the naming function. According to its definition we have to do that incrementally. Meaning that we first calculate <math>\beta_{S_1}</math> then  <math>\beta_{S_2}</math> and finally <math>\beta_{S_3}</math>.
 ===Calculating <math>\beta_{S_1}</math>===
-Since <math>\beta_{S_1}</math> contains only one class it is sufficient to define <math>\beta_{S_1}\left( C_1 \mapsto C_1 \right)</math>. According to the definition:
+Since <math>\beta_{S_1}</math> contains only one class it is sufficient to define <math>\beta_{S_1}\left( A \mapsto A\right)</math>. According to the definition:
 *<math>
     \beta_{S_1}\left( C_1 \mapsto C_1 \right)
        =
-    \mbox{id} \left( \mbox{dom} \left( \tau_1 \right) \right)
+    \mbox{id} \left(
-      \, \cup \,
+      \mbox{dom} \left( \tau_1 \right)
-   \mbox {UNION} \ b \, \cdot \, \left(b \in \alpha_1
+         \, \cup \,
-      \ |\
+      \mbox {UNION} \ b \, \cdot \, \left(b \in \alpha_1
-   \mbox{id} \left( \mbox{ran} \left( \beta_{ S_0 } \left( b \mapsto b \right) \ll \eta_{1, b} \right) \right) \right)
+         \ |\
+      \mbox{ran} \left( \beta_{ S_0 } \left( b \mapsto b \right) \ll \eta_{1, b} \right) \right) \right)
 </math>
 We can forget about the right part of the union since <math>C_1\,</math> has no base classes. So we need to calculate:
@@ Line 131: / Line 152: @@
     \beta_{S_2}\left( C_2 \mapsto C_2 \right)
        =
-    \mbox{id} \left( \mbox{dom} \left( \tau_2 \right) \right)
+    \mbox{id} \left( \mbox{dom} \left( \tau_2 \right)
        \, \cup \,
     \mbox {UNION} \ b \, \cdot \, \left(b \in \alpha_2
        \ |\
-    \mbox{id}\left(\mbox{ran}\left( \beta_{ S_{1} } \left( b \mapsto b \right) \ll \eta_{2, b} \right)\right)
+    \mbox{ran}\left( \beta_{ S_{1} } \left( b \mapsto b \right) \ll \eta_{2, b} \right)\right)
     \right)
 </math>
@@ Line 145: / Line 166: @@
 </math>
 #<math>
-\mbox{id} \left( \mbox{dom} \left( \tau_2 \right) \right) = \left\{ f_2 \mapsto f_2, g_2 \mapsto g_2\right\}
+\mbox{dom} \left( \tau_2 \right) = \left\{ f_2, g_2 \right\}
 </math>
@@ Line 153: / Line 174: @@
 \mbox {UNION} \ b \, \cdot \, \left(b \in \left\{ C_1 \right\}
        \ |\
-    \mbox{id}\left(\mbox{ran}\left( \beta_{ S_{1} } \left( b \mapsto b \right) \ll \eta_{2, b} \right)\right)\right)
+    \mbox{ran}\left( \beta_{ S_{1} } \left( b \mapsto b \right) \ll \eta_{2, b} \right)\right)
 =
-\mbox{id}\left(\mbox{ran}\left( \beta_{ S_{1} } \left( C_1 \mapsto C_1 \right) \ll \eta_{2, C_1} \right)\right)
+\mbox{ran}\left( \beta_{ S_{1} } \left( C_1 \mapsto C_1 \right) \ll \eta_{2, C_1} \right)
 </math>
 #<math>
@@ Line 171: / Line 192: @@
 </math>
 #<math>
-    \mbox{id}\left(\mbox{ran}\left( \left\{ f_1 \mapsto f_2, g_1 \mapsto g_2\right\} \right) \right)
+    \mbox{ran}\left( \left\{ f_1 \mapsto f_2, g_1 \mapsto g_2\right\} \right)
 =
-    \left\{ f_2 \mapsto f_2, g_2 \mapsto g_2\right\}
+    \left\{ f_2, g_2\right\}
 </math>
@@ Line 384: / Line 405: @@
 </math>
-Note that we can ommit <math>\eta_{3,b}\,</math> from the formulas since it is always empty.
+Note that we can omit <math>\eta_{3,b}\,</math> from the formulas since it is always empty.
 #<math>
@@ Line 559: / Line 580: @@
 ==The dynamic binding function==
-To calculate the dynamic binding function, we need to get <math>\delta_{S_3}</math>. We will again calculate it incrementaly:
+To calculate the dynamic binding function, we need to get <math>\delta_{S_3}</math>. We will again calculate it incrementally:
 ===Calculating <math>\delta_{S_1}</math>===
 According to the [[DynBindModel#The_dynamic_binding_function|definition]]:
 <math>
 \delta_{S_1} \left( C_1 \mapsto C_1 \right)
    =
-\left( \mbox {UNION} \, b \, \cdot \, \left(
+\beta_S \left( C_1 \mapsto C_1 \right) ;
+\left(
+\left( \mbox {UNION} \, b \cdot \left(
      b \in \alpha_1
        \, |\,
-     \left( \delta_{ S_{0} } \left( b \mapsto b \right)^{-1} ; \beta_S \left( b \mapsto C_1 \right) \right)^{-1}\right)  \right) \ll \tau_{1}
+     \left( \beta_S \left( b \mapsto b \right) ; \eta_{1,b} \right)^{-1}
+      ;
+    \delta_{S_0}\left( b \mapsto b \right)\right)  \right) \ll \tau_1
+\right)
 </math>
@@ Line 575: / Line 602: @@
 \delta_{S_1} \left( C_1 \mapsto C_1 \right)
    =
-\tau_{1}
+\beta_S \left( C_1 \mapsto C_1 \right) ; \tau_1
-  =
-\tau \left( C_1 \right)
    =
+\left\{ f_1 \mapsto f_1, g_1 \mapsto g_1 \right\}
+  ;
 \left\{ f_1 \mapsto \underline{C_1.f_1}, g_1 \mapsto \underline{C_1.g_1} \right\}
 </math>
@@ Line 590: / Line 617: @@
 \right\}
 </math>
 ===Calculating <math>\delta_{S_2}</math>===
 Again we calculate the different parts of the function in separate sections:
@@ Line 609: / Line 637: @@
 ====Calculate <math>\delta_{S_2}\left( C_2 \mapsto C_2 \right)</math>====
 According to the [[DynBindModel#The_dynamic_binding_function|definition]]:
 <math>
    \delta_{S_2}\left( C_2 \mapsto C_2 \right)
      =
-  \left( \mbox {UNION} \, b \, \cdot \, \left(b \in \alpha_2
+\beta_S \left( C_2 \mapsto C_2 \right) ;
+\left(
+\left( \mbox {UNION} \, b \cdot \left(
+    b \in \alpha_2
        \, |\,
-  \left( \delta_{ S_1 } \left( b \mapsto b \right)^{-1}
+    \left( \beta_S \left( b \mapsto b \right) ; \eta_{2,b} \right)^{-1}
-    ;
+      ;
-  \beta_S \left( b \mapsto C_2 \right) \right)^{-1}\right)  \right) \ll \tau_2
+    \delta_{S_1}\left( b \mapsto b \right)\right)  \right) \ll \tau_2
+\right)
 </math>
 #<math>
-   \left( \mbox {UNION} \, b \cdot \left(b \in \left\{ C_1 \right\}
+   \mbox {UNION} \, b \cdot \left(b \in \left\{ C_1 \right\}
        \, |\,
-  \left( \delta_{ S_1 } \left( b \mapsto b \right)^{-1}
+    \left( \beta_S \left( b \mapsto b \right) ; \eta_{2,b} \right)^{-1}
-    ;
+      ;
-  \beta_S \left( b \mapsto C_2 \right) \right)^{-1}\right)  \right)
+    \delta_{S_1}\left( b \mapsto b \right)\right)
      =
-  \left(
+    \left( \beta_S \left( C_1 \mapsto C_1 \right) ; \eta_{2,C_1} \right)^{-1}
-  \delta_{ S_1 } \left( C_1 \mapsto C_1 \right)^{-1}
+      ;
-    ;
+    \delta_{S_1}\left( C_1 \mapsto C_1 \right)
-  \beta_S \left( C_1 \mapsto C_2 \right) \right)^{-1}
 </math>
 ##<math>
-   \delta_{ S_1 } \left( C_1 \mapsto C_1 \right)^{-1}
+   \beta_S \left( C_1 \mapsto C_1 \right) ; \eta_{2,C_1}
      =
-   \left\{ \underline{C_1.f_1} \mapsto f_1, \underline{C_1.g_1} \mapsto g_1 \right\}
+   \left\{ f_1 \mapsto f_2, g_1 \mapsto g_2 \right\}
 </math>
 ##<math>
-   \delta_{ S_1 } \left( C_1 \mapsto C_1 \right)^{-1}
+   \left( \beta_S \left( C_1 \mapsto C_1 \right) ; \eta_{2,C_1} \right)^{-1}
-    ;
-  \beta_S \left( C_1 \mapsto C_2 \right)
      =
-   \left\{ \underline{C_1.f_1} \mapsto f_2, \underline{C_1.g_1} \mapsto g_2 \right\}
+   \left\{ f_2 \mapsto f_1, g_2 \mapsto g_1 \right\}
 </math>
 ##<math>
-   \left(
+   \left( \beta_S \left( C_1 \mapsto C_1 \right) ; \eta_{2,C_1} \right)^{-1}
-  \delta_{ S_1 } \left( C_1 \mapsto C_1 \right)^{-1}
+      ;
-    ;
+   \delta_{S_1}\left( C_1 \mapsto C_1 \right)
-  \beta_S \left( C_1 \mapsto C_2 \right) \right)^{-1}
      =
   \left\{ f_2 \mapsto \underline{C_1.f_1}, g_2 \mapsto \underline{C_1.g_1} \right\}
@@ Line 677: / Line 706: @@
    \delta_{S_2}\left( C_1 \mapsto C_2 \right)
      =
-\mbox {UNION} \, b \cdot
+\beta_S \left( C_1 \mapsto C_2 \right) ;
 \left(
-     b \in \alpha_m
+\left( \mbox {UNION} \, b \cdot \left(
+     b \in \alpha_2
        \, |\,
-     \beta_S \left( C_1 \mapsto C_2 \right);
+     \left( \beta_S \left( b \mapsto b \right) ; \eta_{2,b} \right)^{-1}
-    \left( \left(
+      ;
-       \delta_{ S_1 } \left( C_1 \mapsto b \right)^{-1}
+    \delta_{S_{1}}\left( b \mapsto b \right)\right)  \right) \ll \tau_{2}
-          ;
+\right)
-       \beta_S \left( C_1 \mapsto C_2 \right) \right)^{-1}
-         \ll
-       \tau_{2} \right)
-\right)
 </math>

DynBindModelExamples: Difference between revisions

Latest revision as of 10:11, 11 April 2007

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)

The complete naming function

The dynamic binding 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

Deriving the dynamic binding function

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})$

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}}$