DynBindModelExamples

2006-11-24T21:44:37Z

Bheilig: class C2 was inheriting from an unknown class 'B'. I assume this was supposed to be C1

[[Category:ECMA]]
Author: Matthias Konrad
==The system==
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"
|-valign="top" -halign="center"
|<code>[eiffel, N]
class
C1
feature
f1 do ... end
g1 do ... end
end
</code>
|
<code>[eiffel, N]
class
C2
inherit
C1
rename f1 as f2, g1 as g2
redefine f2, g2 end
feature
f2 do ... end
g2 do ... end
end
</code>
|
<code>[eiffel, N]
class
C3
inherit
C2
select f2 end
C1
redefine f1, g1
select g1 end
feature
f1 do ... end
g1 do ... end
end
</code>
|}
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>\tau =
\left\{
C_1 \mapsto \left\{ f_1 \mapsto \underline{C_1.f_1}, g_1 \mapsto \underline{C_1.g_1} \right\},
C_2 \mapsto \left\{ f_2 \mapsto \underline{C_2.f_2}, g_2 \mapsto \underline{C_2.g_2} \right\},
C_3 \mapsto \left\{ f_1 \mapsto \underline{C_3.f_1}, g_1 \mapsto \underline{C_3.g_1} \right\}
\right\}
</math>
*<math>\eta =
\left\{
C_2 \mapsto \left\{
C_1 \mapsto \left\{ f_1 \mapsto f_2, g_1 \mapsto g_2 \right\}
\right\}
\right\}
</math>
*<math>\alpha = \left\{
C_2 \mapsto \left\{ C_1 \right\},
C_3 \mapsto \left\{ C_2, C_1 \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\}
\right\}
</math>

==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 <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:

*<math>
\beta_{S_1}\left( C_1 \mapsto C_1 \right)
=
\mbox{id} \left( \mbox{dom} \left( \tau_1 \right) \right)
\, \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)
</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:
#<math>\mbox{id} \left( \mbox{dom} \left( \tau_1 \right) \right) </math>
##<math>
\tau_1 = \tau (C_1) = \left\{ f_1 \mapsto \underline{C_1.f_1}, g_1 \mapsto \underline{C_1.g_1} \right\}
</math>
##<math>
\mbox{dom} \left( \tau_1 \right) = \left\{ f_1, g_1 \right\}
</math>
##<math>
\mbox{id} \left( \mbox{dom} \left( \tau_1 \right) \right) = \left\{ f_1 \mapsto f_1, g_1 \mapsto g_1\right\}
</math>

So we get:

<math>
\beta_{S_1}\left( C_1 \mapsto C_1 \right) = \left\{ f_1 \mapsto f_1, g_1 \mapsto g_1\right\}
</math>

And hence:

<math>
\beta_{S_1} = \left\{ \left( C_1 \mapsto C_1 \right) \mapsto
\left\{ f_1 \mapsto f_1, g_1 \mapsto g_1 \right\} \right\}
</math>

===Calculating <math>\beta_{S_2}</math>===

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

====Calculate <math>\beta_{S_2}\left( C_1 \mapsto C_1 \right)</math>====
According to the [[DynBindModel#The_naming_function|definition]]:
<math>
\beta_{S_2}\left( C_1 \mapsto C_1 \right) =
\beta_{S_1}\left( C_1 \mapsto C_1 \right) = \left\{ f_1 \mapsto f_1, g_1 \mapsto g_1\right\}
</math>

====Calculate <math>\beta_{S_2}\left( C_2 \mapsto C_1 \right)</math>====
According to the [[DynBindModel#The_naming_function|definition]]:
<math>
\beta_{S_2}\left( C_2 \mapsto C_1 \right) = \emptyset
</math>

====Calculate <math>\beta_{S_2}\left( C_2 \mapsto C_2 \right)</math>====
According to the [[DynBindModel#The_naming_function|definition]]:
<math>
\beta_{S_2}\left( C_2 \mapsto C_2 \right)
=
\mbox{id} \left( \mbox{dom} \left( \tau_2 \right) \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)
\right)
</math>

Lets calculate the left part first:

#<math>
\tau_2 = \tau (C_2) = \left\{ f_2 \mapsto \underline{C_2.f_2}, g_2 \mapsto \underline{C_2.g_2} \right\}
</math>
#<math>
\mbox{id} \left( \mbox{dom} \left( \tau_2 \right) \right) = \left\{ f_2 \mapsto f_2, g_2 \mapsto g_2\right\}
</math>

And now the right part:

#<math>
\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{id}\left(\mbox{ran}\left( \beta_{ S_{1} } \left( C_1 \mapsto C_1 \right) \ll \eta_{2, C_1} \right)\right)
</math>
#<math>
\beta_{ S_{1} } \left( C_1 \mapsto C_1 \right)
=
\left\{ f_1 \mapsto f_1, g_1 \mapsto g_1\right\}
</math>
#<math>
\eta_{2,C_1} = \eta (C_2)(C_1) = \left\{ f_1 \mapsto f_2, g_1 \mapsto g_2 \right\}
</math>
#<math>
\left\{ f_1 \mapsto f_1, g_1 \mapsto g_1\right\} \ll \left\{ f_1 \mapsto f_2, g_1 \mapsto g_2 \right\}
=
\left\{ f_1 \mapsto f_2, g_1 \mapsto g_2 \right\}
</math>
#<math>
\mbox{id}\left(\mbox{ran}\left( \left\{ f_1 \mapsto f_2, g_1 \mapsto g_2\right\} \right) \right)
=
\left\{ f_2 \mapsto f_2, g_2 \mapsto g_2\right\}
</math>

So we get:

<math>
\beta_{S_2} \left( C_2 \mapsto C_2 \right)
=
\left\{ f_2 \mapsto f_2, g_2 \mapsto g_2\right\}
</math>

====Calculate <math>\beta_{S_2} \left( C_1 \mapsto C_2 \right)</math>====
According to the [[DynBindModel#The_naming_function|definition]]:
<math>
\beta_{S_2} \left( C_1 \mapsto C_2 \right)
=
{\beta_{S_2}}^\prime \left( C_1 \mapsto C_2 \right)
\ll
\theta_{S_2} \left( C_1 \mapsto C_2 \right)
</math>

Where:
<math>
{\beta_{S_2}}^\prime \left( C_1 \mapsto C_2 \right)
=
\mbox {UNION} \ b \ \cdot \ \left(
b \in \alpha_2
\ |\
\beta_{S_{1}} \left( C_1 \mapsto b \right)
;
\left(
\mbox{id} \left( \mbox{ran} \left( \beta_{S_{1}} \left( C_1 \mapsto b \right) \right) \right)
\ll
\eta_{2,b}
\right)
\right)
</math>

And:
<math>
\theta_{S_2} \left( C_1 \mapsto C_2 \right)
=
\mbox {UNION} \ b \ \cdot \ \left(
b \in \alpha_2
\ |\
\beta_{S_{1}} \left( C_1 \mapsto b \right)
;
\left(
\mbox{id} \left( \mbox{ran} \left( \beta_{S_1} \left( C_1 \mapsto b \right) \right) \right)
\ll
\eta_{2,b}
\right)
\triangleright \sigma_{2,b}
\right)
</math>

Here are the steps taken to compute the part:

#<math>
\beta_{S_{1}} \left( C_1 \mapsto C_1 \right)
;
\left(
\mbox{id} \left( \mbox{ran} \left( \beta_{S_{1}} \left( C_1 \mapsto C_1 \right) \right) \right)
\ll
\eta_{2,C_1}
\right)
</math>
##<math>
\mbox{id} \left( \mbox{ran} \left( \beta_{S_{1}} \left( C_1 \mapsto C_1 \right) \right) \right)
=
\left\{ f_1 \mapsto f_1, g_1 \mapsto g_1 \right\}
</math>
##<math>
\left\{ f_1 \mapsto f_1, g_1 \mapsto g_1 \right\} \ll \left\{ f_1 \mapsto f_2, g_1 \mapsto g_2 \right\}
=
\left\{ f_1 \mapsto f_2, g_1 \mapsto g_2 \right\}
</math>
##<math>
\left\{ f_1 \mapsto f_1, g_1 \mapsto g_1 \right\} \,;\, \left\{ f_1 \mapsto f_2, g_1 \mapsto g_2 \right\}
=
\left\{ f_1 \mapsto f_2, g_1 \mapsto g_2 \right\}
</math>
##<math>
{\beta_{S_2}}^\prime \left( C_1 \mapsto C_2 \right)
=
\left\{ f_1 \mapsto f_2, g_1 \mapsto g_2 \right\}
</math>
#<math>
\beta_{S_1} \left( C_1 \mapsto C_1 \right)
;
\left(
\mbox{id} \left( \mbox{ran} \left( \beta_{S_1} \left( C_1 \mapsto C_1 \right) \right) \right)
\ll
\eta_{2,C_1}
\right)
\triangleright \sigma_{2,C_1}
</math>
##<math>
\sigma_{2,C_1} = \emptyset
</math>
##<math>
\mbox{id} \left( \mbox{ran} \left( \beta_{S_1} \left( C_1 \mapsto C_1 \right) \right) \right)
\ll
\emptyset
=
\emptyset
</math>
##<math>
\beta_{S_1} \left( C_1 \mapsto C_1 \right)
;
\emptyset
=
\emptyset
</math>
##<math>
\theta_{S_2} \left( C_1 \mapsto C_2 \right) = \emptyset
</math>
# <math>
\left\{ f_1 \mapsto f_2, g_1 \mapsto g_2 \right\} \ll \emptyset
=
\left\{ f_1 \mapsto f_2, g_1 \mapsto g_2 \right\}
</math>

So we get:

<math>
\beta_{S_2} \left( C_1 \mapsto C_2 \right)
=
\left\{ f_1 \mapsto f_2, g_1 \mapsto g_2 \right\}
</math>

====Putting the parts together:====
We can know show the complete total function:

{|border="0" cellpadding="2" cellspacing="0" align="center"
|-valign="top" -halign="center"
|
<math>\beta_{S_2} = \{</math>
|
<math>
\left( C_1 \mapsto C_1 \right) \mapsto \left\{ f_1 \mapsto f_1, g_1 \mapsto g_1 \right\},
</math>
|-
||
|
<math>
\left( C_1 \mapsto C_2 \right) \mapsto \left\{ f_1 \mapsto f_2, g_1 \mapsto g_2 \right\},
</math>
|-
||
|
<math>
\left( C_2 \mapsto C_1 \right) \mapsto \emptyset,
</math>
|-
||
|
<math>
\left( C_2 \mapsto C_2 \right) \mapsto \left\{ f_2 \mapsto f_2, g_2 \mapsto g_2 \right\} \ \}
</math>

|}

===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 parts.

====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)
=
{\beta_{S_3}}^\prime \left( C_1 \mapsto C_3 \right)
\ll
\theta_{S_3} \left( C_1 \mapsto C_3 \right)
</math>

Where:
<math>
{\beta_{S_3}}^\prime \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)
\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>

Note that we can omit <math>\eta_{3,b}\,</math> from the formulas since it is always empty.

#<math>
\beta_{S_2} \left( C_1 \mapsto C_2 \right)
;
\mbox{id} \left( \mbox{ran} \left( \beta_{S_2} \left( C_1 \mapsto C_2 \right) \right) \right)
\ \cup \
\beta_{S_2} \left( C_1 \mapsto C_1 \right)
;
\mbox{id} \left( \mbox{ran} \left( \beta_{S_2} \left( C_1 \mapsto C_1 \right) \right) \right)
</math>
##<math>
\beta_{S_{2}} \left( C_1 \mapsto C_2 \right)
=
\left\{ f_1 \mapsto f_2, g_1 \mapsto g_2 \right\}
</math>
##<math>
\mbox{id}\left(\mbox{ran}\left( \beta_{S_{2}} \left( C_1 \mapsto C_2 \right) \right)\right)
=
\left\{ f_2 \mapsto f_2, g_2 \mapsto g_2 \right\}
</math>
##<math>
\beta_{S_2} \left( C_1 \mapsto C_2 \right)
;
\mbox{id} \left( \mbox{ran} \left( \beta_{S_2} \left( C_1 \mapsto C_2 \right) \right) \right)
=
\left\{ f_1 \mapsto f_2, g_1 \mapsto g_2 \right\}
</math>
##<math>
\beta_{S_{2}} \left( C_1 \mapsto C_1 \right)
=
\left\{ f_1 \mapsto f_1, g_1 \mapsto g_1 \right\}
</math>
##<math>
\mbox{id}\left(\mbox{ran}\left( \beta_{S_{2}} \left( C_1 \mapsto C_1 \right) \right)\right)
=
\left\{ f_1 \mapsto f_1, g_1 \mapsto g_1 \right\}
</math>
##<math>
\beta_{S_2} \left( C_1 \mapsto C_1 \right)
;
\mbox{id} \left( \mbox{ran} \left( \beta_{S_2} \left( C_1 \mapsto C_1 \right) \right) \right)
=
\left\{ f_1 \mapsto f_1, g_1 \mapsto g_1 \right\}
</math>
##<math>
\left\{ f_1 \mapsto f_2, g_1 \mapsto g_2 \right\}
\ \cup\
\left\{ f_1 \mapsto f_1, g_1 \mapsto g_1 \right\}
=
\left\{ f_1 \mapsto f_1, f_1 \mapsto f_2, g_1 \mapsto g_1, g_1 \mapsto g_2 \right\}
</math>
#<math>
\beta_{S_2} \left( C_1 \mapsto C_2 \right)
;
\mbox{id} \left( \mbox{ran} \left( \beta_{S_2} \left( C_1 \mapsto C_2 \right) \right) \right)
\ \triangleright\
\sigma_{3,C_2}
\ \cup \
\beta_{S_2} \left( C_1 \mapsto C_1 \right)
;
\mbox{id} \left( \mbox{ran} \left( \beta_{S_2} \left( C_1 \mapsto C_1 \right) \right) \right)
\ \triangleright\
\sigma_{3,C_1}
</math>
##<math>
\sigma_{3,C_2} = \sigma \left(C_3 \right) \left(C_2\right) = \left\{ f_2 \right\}
</math>
##<math>
\sigma_{3,C_1} = \sigma \left(C_3 \right) \left(C_1\right) = \left\{ g_1 \right\}
</math>
##<math>
\beta_{S_2} \left( C_1 \mapsto C_2 \right)
;
\mbox{id} \left( \mbox{ran} \left( \beta_{S_2} \left( C_1 \mapsto C_2 \right) \right) \right)
\ \triangleright\
\sigma_{3,C_2}
=
\left\{ f_1 \mapsto f_2 \right\}
</math>
##<math>
\beta_{S_2} \left( C_1 \mapsto C_1 \right)
;
\mbox{id} \left( \mbox{ran} \left( \beta_{S_2} \left( C_1 \mapsto C_1 \right) \right) \right)
\ \triangleright\
\sigma_{3,C_1}
=
\left\{ g_1 \mapsto g_1 \right\}
</math>
##<math>
\left\{ f_1 \mapsto f_2 \right\} \ \cup \ \left\{ g_1 \mapsto g_1 \right\}
=
\left\{ f_1 \mapsto f_2, g_1 \mapsto g_1 \right\}
</math>
##<math>
\left\{ f_1 \mapsto f_1, f_1 \mapsto f_2, g_1 \mapsto g_1, g_1 \mapsto g_2 \right\}
\ll
\left\{ f_1 \mapsto f_2, g_1 \mapsto g_1 \right\}
=
\left\{ f_1 \mapsto f_2, g_1 \mapsto g_1 \right\}
</math>

So we get:

<math>
\beta_{S_3} \left( C_1 \mapsto C_3 \right)
=
\left\{ f_1 \mapsto f_2, g_1 \mapsto g_1 \right\}
</math>

====The complete naming function====

{|border="0" cellpadding="2" cellspacing="0" align="center"
|-valign="top" -halign="center"
|
<math>\beta_{S_3} = \{</math>
|
<math>
\left( C_1 \mapsto C_1 \right) \mapsto \left\{ f_1 \mapsto f_1, g_1 \mapsto g_1 \right\},
</math>
|-
||
|
<math>
\left( C_1 \mapsto C_2 \right) \mapsto \left\{ f_1 \mapsto f_2, g_1 \mapsto g_2 \right\},
</math>
|-
||
|
<math>
\left( C_2 \mapsto C_1 \right) \mapsto \emptyset,
</math>
|-
||
|
<math>
\left( C_2 \mapsto C_2 \right) \mapsto \left\{ f_2 \mapsto f_2, g_2 \mapsto g_2 \right\},
</math>
|-
||
|
<math>
\left( C_1 \mapsto C_3 \right) \mapsto \left\{ f_1 \mapsto f_2, g_1 \mapsto g_1 \right\},
</math>
|-
||
|
<math>
\left( C_2 \mapsto C_3 \right) \mapsto \left\{ f_2 \mapsto f_2, g_2 \mapsto g_2 \right\},
</math>
|-
||
|
<math>
\left( C_3 \mapsto C_3 \right)
\mapsto
\left\{ f_1 \mapsto f_1, g_1 \mapsto g_1, f_2 \mapsto f_2, g_2 \mapsto g_2 \right\},
</math>
|-
||
|
<math>
\left( C_3 \mapsto C_1 \right) \mapsto \emptyset,
</math>
|-
||
|
<math>
\left( C_3 \mapsto C_2 \right) \mapsto \emptyset \ \}
</math>

|}

==The dynamic binding function==
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)
=
\beta_S \left( C_1 \mapsto C_1 \right) ;
\left(
\left( \mbox {UNION} \, b \cdot \left(
b \in \alpha_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>

Since <math>\alpha_1\,</math> is empty this simplifies to:
<math>
\delta_{S_1} \left( C_1 \mapsto C_1 \right)
=
\beta_S \left( C_1 \mapsto C_1 \right) ; \tau_1
=
\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>

So we get:
<math>
\delta_{S_1}
=
\left\{ \left( C_1 \mapsto C_1 \right) \mapsto
\left\{ f_1 \mapsto \underline{C_1.f_1}, g_1 \mapsto \underline{C_1.g_1} \right\}
\right\}
</math>

===Calculating <math>\delta_{S_2}</math>===
Again we calculate the different parts of the function in separate sections:

====Calculate <math>\delta_{S_2}\left( C_1 \mapsto C_1 \right)</math>====
According to the [[DynBindModel#The_dynamic_binding_function|definition]]:
<math>
\delta_{S_2}\left( C_1 \mapsto C_1 \right) =
\delta_{S_1}\left( C_1 \mapsto C_1 \right) =
\left\{ f_1 \mapsto \underline{C_1.f_1}, g_1 \mapsto \underline{C_1.g_1} \right\}
</math>

====Calculate <math>\delta_{S_2}\left( C_2 \mapsto C_1 \right)</math>====
According to the [[DynBindModel#The_dynamic_binding_function|definition]]:
<math>
\delta_{S_2}\left( C_1 \mapsto C_1 \right) = \emptyset
</math>

====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)
=
\beta_S \left( C_2 \mapsto C_2 \right) ;
\left(
\left( \mbox {UNION} \, b \cdot \left(
b \in \alpha_2
\, |\,
\left( \beta_S \left( b \mapsto b \right) ; \eta_{2,b} \right)^{-1}
;
\delta_{S_1}\left( b \mapsto b \right)\right) \right) \ll \tau_2
\right)
</math>

#<math>
\mbox {UNION} \, b \cdot \left(b \in \left\{ C_1 \right\}
\, |\,
\left( \beta_S \left( b \mapsto b \right) ; \eta_{2,b} \right)^{-1}
;
\delta_{S_1}\left( b \mapsto b \right)\right)
=
\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)
</math>
##<math>
\beta_S \left( C_1 \mapsto C_1 \right) ; \eta_{2,C_1}
=
\left\{ f_1 \mapsto f_2, g_1 \mapsto g_2 \right\}
</math>
##<math>
\left( \beta_S \left( C_1 \mapsto C_1 \right) ; \eta_{2,C_1} \right)^{-1}
=
\left\{ f_2 \mapsto f_1, g_2 \mapsto g_1 \right\}
</math>
##<math>
\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)
=
\left\{ f_2 \mapsto \underline{C_1.f_1}, g_2 \mapsto \underline{C_1.g_1} \right\}
</math>
#<math>
\tau_2 = \tau \left( C_2 \right)
=
\left\{ f_2 \mapsto \underline{C_2.f_2}, g_2 \mapsto \underline{C_2.g_2} \right\}
</math>
#<math>
\left\{ f_2 \mapsto \underline{C_1.f_1}, g_2 \mapsto \underline{C_1.g_1} \right\}
\ll
\left\{ f_2 \mapsto \underline{C_2.f_2}, g_2 \mapsto \underline{C_2.g_2} \right\}
=
\left\{ f_2 \mapsto \underline{C_2.f_2}, g_2 \mapsto \underline{C_2.g_2} \right\}
</math>

So we get:
<math>
\delta_{S_2}\left( C_2 \mapsto C_2 \right)
=
\left\{ f_2 \mapsto \underline{C_2.f_2}, g_2 \mapsto \underline{C_2.g_2} \right\}
</math>

====Calculate <math>\delta_{S_2}\left( C_1 \mapsto C_2 \right)</math>====
According to the [[DynBindModel#The_dynamic_binding_function|definition]]:

<math>
\delta_{S_2}\left( C_1 \mapsto C_2 \right)
=
\beta_S \left( C_1 \mapsto C_2 \right) ;
\left(
\left( \mbox {UNION} \, b \cdot \left(
b \in \alpha_2
\, |\,
\left( \beta_S \left( b \mapsto b \right) ; \eta_{2,b} \right)^{-1}
;
\delta_{S_{1}}\left( b \mapsto b \right)\right) \right) \ll \tau_{2}
\right)
</math>

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

<math>
\delta_{S_2}\left( C_1 \mapsto C_2 \right)
=
\left\{ f_1 \mapsto \underline{C_2.f_2}, g_1 \mapsto \underline{C_2.g_2} \right\}
</math>

====Putting the parts together:====
We can know show the complete total function:

{|border="0" cellpadding="2" cellspacing="0" align="center"
|-valign="top" -halign="center"
|
<math>\delta_{S_2} = \{</math>
|
<math>
\left( C_1 \mapsto C_1 \right)
\mapsto
\left\{ f_1 \mapsto \underline{C_1.f_1}, g_1 \mapsto \underline{C_1.g_1} \right\},
</math>
|-
||
|
<math>
\left( C_1 \mapsto C_2 \right)
\mapsto
\left\{ f_1 \mapsto \underline{C_2.f_2}, g_1 \mapsto \underline{C_2.g_2} \right\},
</math>
|-
||
|
<math>
\left( C_2 \mapsto C_1 \right) \mapsto \emptyset,
</math>
|-
||
|
<math>
\left( C_2 \mapsto C_2 \right)
\mapsto
\left\{ f_2 \mapsto \underline{C_2.f_2}, g_2 \mapsto \underline{C_2.g_2} \right\} \ \}
</math>
|}
===Calculating <math>\delta_{S_3}</math>===
There is nothing new for this calculation so we just present the result:
{|border="0" cellpadding="2" cellspacing="0" align="center"
|-valign="top" -halign="center"
|
<math>\delta_{S_3} = \{</math>
|
<math>
\left( C_1 \mapsto C_1 \right)
\mapsto
\left\{ f_1 \mapsto \underline{C_1.f_1}, g_1 \mapsto \underline{C_1.g_1} \right\},
</math>
|-
||
|
<math>
\left( C_1 \mapsto C_2 \right)
\mapsto
\left\{ f_1 \mapsto \underline{C_2.f_2}, g_1 \mapsto \underline{C_2.g_2} \right\},
</math>
|-
||
|
<math>
\left( C_2 \mapsto C_1 \right) \mapsto \emptyset,
</math>
|-
||
|
<math>
\left( C_2 \mapsto C_2 \right)
\mapsto
\left\{ f_2 \mapsto \underline{C_2.f_2}, g_2 \mapsto \underline{C_2.g_2} \right\},
</math>
|-
||
|
<math>
\left( C_1 \mapsto C_3 \right)
\mapsto
\left\{ f_1 \mapsto \underline{C_2.f_2}, g_1 \mapsto \underline{C_3.g_1} \right\},
</math>
|-
||
|
<math>
\left( C_2 \mapsto C_3 \right)
\mapsto
\left\{ f_2 \mapsto \underline{C_2.f_2}, g_2 \mapsto \underline{C_2.g_2} \right\},
</math>
|-
||
|
<math>
\left( C_3 \mapsto C_3 \right)
\mapsto
\left\{ 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} \right\},
</math>
|-
||
|
<math>
\left( C_3 \mapsto C_1 \right) \mapsto \emptyset,
</math>
|-
||
|
<math>
\left( C_3 \mapsto C_2 \right) \mapsto \emptyset \ \}
</math>
|}
===Deriving the dynamic binding function===
The function is now given. We evaluate it at two interesting points:

*<math>
\delta\left( C_1 \mapsto f_1 \right)
=
\left\{
C_1 \mapsto \underline{C_1.f_1}, C_2 \mapsto \underline{C_2.f_2}, C_3 \mapsto \underline{C_2.f_2}
\right\}
</math>

*<math>
\delta\left( C_1 \mapsto f_g \right)
=
\left\{
C_1 \mapsto \underline{C_1.f_g}, C_2 \mapsto \underline{C_2.g_2}, C_3 \mapsto \underline{C_2.g_1}
\right\}
</math>

Downloads

2006-04-07T19:27:07Z

Bheilig: /* EiffelStudio 5.7 Pre-releases */

==EiffelStudio 5.7 Pre-releases==
We currently provide versions of EiffelStudio for Windows and Linux (both 32 and 64-bit). Choose the version of your choice below:
* [http://eiffelsoftware.origo.ethz.ch/builds/Eiffel57_0826_linux-x86.tgz Linux 32-bit]
* [http://eiffelsoftware.origo.ethz.ch/builds/Eiffel57_0826_linux-x86-64.tgz Linux 64-bit]
* [http://eiffelsoftware.origo.ethz.ch/builds/Eiffel57_0826_windows.msi Windows 32-bit]
* [http://eiffelsoftware.origo.ethz.ch/builds/Eiffel57_0826_win64.msi Windows 64-bit]

While waiting for a new drop of the 5.7 release, the Linux version requires a CD-key, contact [http://www.eiffel.com/general/contact_details.html Eiffel Software] to get one.

The documentation is a work in progress and the included documentation in the above packages does not reflect changes made in the new EiffelStudio 5.7 release.

To access older builds, go directly to http://eiffelsoftware.origo.ethz.ch/builds/OLD_RELEASES

==EiffelStudio 5.6==
You can download the official EiffelStudio 5.6 release from [http://www.eiffel.com/downloads/eiffelstudio.html Eiffel Software].

Downloads

2006-04-07T19:26:44Z

Bheilig: /* EiffelStudio 5.7 Pre-releases */

==EiffelStudio 5.7 Pre-releases==
We currently provide versions of EiffelStudio for Windows and Linux (both 32 and 64-bit). Choose the version of your choice below:
* [http://eiffelsoftware.origo.ethz.ch/builds/Eiffel57_0826_linux-x86.tgz Linux 32-bit]
* [http://eiffelsoftware.origo.ethz.ch/builds/Eiffel57_0826_linux-x86-64.tgz Linux 64-bit]
* [http://eiffelsoftware.origo.ethz.ch/builds/Eiffel57_0826_windows.msi Windows 32-bit]
* [http://eiffelsoftware.origo.ethz.ch/builds/Eiffel57_0826_win64.msi Windows 64-bit]

While waiting for a new drop of the 5.7 release, the Linux version requires a CD-key, contact [http://www.eiffel.com/general/contact_details.html Eiffel Software] to get one.

The documentation is a work in progress and the included documentation in the above packages does not reflect changes made in the new EiffelStudio 5.7 release.

To access to older builds, go directly to http://eiffelsoftware.origo.ethz.ch/builds/OLD_RELEASES

==EiffelStudio 5.6==
You can download the official EiffelStudio 5.6 release from [http://www.eiffel.com/downloads/eiffelstudio.html Eiffel Software].

EiffelStudio: an EiffelSoftware project - User contributions [en]

DynBindModelExamples

Downloads

Downloads