DynBindModelExamples: Difference between revisions

Revision as of 18:38, 11 October 2006

Author: Matthias Konrad

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 f2 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_{2}}, C_{1} \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))
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} | 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 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 ommit $η_{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 incrementaly:

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}) = UNION b \cdot (b \in α_{m} | β_{S} (C_{1} \mapsto C_{2}); ({(δ_{S_{1}} {(C_{1} \mapsto b)}^{- 1}; β_{S} (C_{1} \mapsto C_{2}))}^{- 1} ≪ τ_{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}}}$

@@ Line 616: / Line 616: @@
 ====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\}

DynBindModelExamples: Difference between revisions

Revision as of 18:38, 11 October 2006

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

DynBindModelExamples: Difference between revisions

Revision as of 18:38, 11 October 2006

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