DynBindModel

Motivation:

Eiffels dynamic binding is somewhat more complex than that of other languages. Its structure is still very simple and can be described by giving the relation:

$\gamma :(\text{TYPE}\times \text{NAME})\to (\text{TYPE}\to \text{FEATURE})$

Relation $\gamma$ contains both the static and dynamic binding part of the language. In the following feature:

f (a: ANY)
   do
      print (a.out)
   end

The static binding part of call a.out can be decribed as:

$\gamma (\text{ANY}\mapsto \text{out})$

Namely an evaluation of $\gamma$ with a tuple containing the static type of the call and the name. The result of this is a function. This function evaluated at runtime will yield the right feature according to the dynamic type of a.

In the rest of this text, the we will show how to construct the relation $\gamma$ based on any given valid Eiffel system.

Notation

This wiki uses the notation introduced in these slided by Prof. Jean-Raymond Abrial (ETHZ): notation The only difference is the symbol for override which is $\ll$ (This will be changed as soon as possible).

Some fundamentals

We introduce the operator $>$ as the "ancestor of" and $<$ as "descendant of" operator.

Without loss of generality we can say that any Eiffel system $S$ is a set of classes $\{C_1,C_2\dots C_n\}$ such that $C_q<C_p$ if $q<p$. In practice class $C_1$ will allways be class ANY but this is not of importance here.

The function:

• $\tau :\text{TYPE}\to (\text{NAME}\to \text{FEATURE})$

Yields the features declared in a given class.

• $\eta :\text{TYPE}\to (\text{TYPE}\to (\text{NAME}\to \text{NAME}))$

Yields the renamings of the different parent parts by a class:

$\eta \left(D\right)\left(B\right)$ gives the renamings in class D for the inherited class B.

• $\alpha :\text{TYPE}\to \mathbb{\mathbb{P}}\left(\text{TYPE}\right)$

Gives the classes from which a given class inherits:

$\alpha \left(A\right)$ Gives the base classes of the of class A.

• $\sigma :\text{TYPE}\to (\text{TYPE}\to \mathbb{\mathbb{P}}\left(\text{NAME}\right))$

Gives all the selected feature names of an inherited class of a class.

Furthermore we give the following shortcuts:

• ${\tau }_n$ for $\tau \left(C_n\right)$
• ${\eta }_{n,b}$ for $\eta \left(C_n\right)\left(b\right)$
• ${\alpha }_n$ for $\alpha \left(C_n\right)$
• ${\sigma }_{n,b}$ for $\sigma \left(C_n\right)\left(b\right)$

An example

For the following System:

class B feature f do ... end end

class C inherit B rename f as f1 redefine f1 end feature f1 do ... end end

class D inherit C select f1 end B rename f as f2 redefine f2 end B rename f as f3 redefine f3 end feature f2 do ... end f3 do ... end end

We get:

• $S=\{B,C,D\}$
• $\tau =\{B\mapsto \{f\mapsto \underset{\_}{B.f}\},C\mapsto \{f1\mapsto \underset{\_}{C.f1}\},D\mapsto \{f2\mapsto \underset{\_}{D.f2},f3\mapsto \underset{\_}{D.f3}\}\}$
• $\eta =\{C\mapsto \{B\mapsto \{f\mapsto f1\}\},D\mapsto \{B\mapsto \{f\mapsto f2,f\mapsto f3\}\}\}$
• $\alpha =\{C\mapsto \left\{B\right\},D\mapsto \{B,C\}\}$
• $\sigma =\{D\mapsto \{C\mapsto \left\{f1\right\}\}\}$

The naming function

In this section the naming function of a system is shown:

Its structure

${\beta }_S:(\text{TYPE}\times \text{TYPE})\to (\text{NAME}\to \text{NAME})$

The range of ${\beta }_S$ is a function. This means, that every name is mapped to just one name. The naming function doesn't only reflect the renaming semantics of a system but also the selects.

We will give a recursive definition of ${\beta }_S$. Meaning that we will give ${\beta }_{\{C_1,\dots C_m\}}$ given that we already now ${\beta }_{\{C_1,\dots C_{m-1}\}}$

This is valid since:

${\beta }_{\left\{C_1\right\}}\subseteq {\beta }_{\{C_1,C_2\}}\subseteq \dots {\beta }_S$

An example

Before we proceed to the definition we show how ${\beta }_{\{B,C,D\}}$ looks like for the example from the previous section:

${\beta }_{\{B,C,D\}}=\{$	$(B\mapsto B)\mapsto \{f\mapsto f\},(B\mapsto C)\mapsto \{f\mapsto f1\},(B\mapsto D)\mapsto \{f\mapsto f1\},$
	$(C\mapsto C)\mapsto \{f1\mapsto f1\},(C\mapsto D)\mapsto \{f1\mapsto f1\},$
	$(D\mapsto D)\mapsto \{f1\mapsto f1,f2\mapsto f2,f3\mapsto f3\}\}$

Its definition

We introduce the shortcut $S_m$ to denote the system $\{C_1\dots C_m\}$

As a helper function we also need these functions:

• ${{\beta }_S}^{\prime }:(\text{TYPE}\times \text{TYPE})\to (\text{NAME}\leftrightarrow \text{NAME})$
• ${{\theta }_S}^{\prime }:(\text{TYPE}\times \text{TYPE})\to (\text{NAME}\to \text{NAME})$

And finally the naming function:

${\beta }_{S_m}(C_q\mapsto C_p)=\{\begin{array}{ll}\mathrm{\varnothing }& \text{if }q>p\\ {\beta }_{S_{m-1}}(C_q\mapsto C_p)& \text{if }q<=p<m\\ \text{id}\left(\text{dom}\left({\tau }_m\right)\right)\cup \text{UNION}b\cdot (b\in {\alpha }_m|{\beta }_{S_{m-1}}(b\mapsto b)\ll {\eta }_{m,b})& \text{if }q=p=m\\ {{\beta }_{S_m}}^{\prime }(C_q\mapsto C_m)\ll {\theta }_{S_m}(C_q\mapsto C_m)& \text{otherwise }\end{array}$

Where

${{\beta }_{S_m}}^{\prime }(C_q\mapsto C_m)=\text{UNION}b\cdot (b\in {\alpha }_m|{\beta }_{S_{m-1}}(C_q\mapsto b);(\text{id}\left(\text{ran}\left({\beta }_{S_{m-1}}(C_q\mapsto b)\right)\right)\ll {\eta }_{m,b}))$

And:

${\theta }_{S_m}(C_q\mapsto C_m)=\text{UNION}b\cdot (b\in {\alpha }_m|{\beta }_{S_{m-1}}(C_q\mapsto b);(\text{id}\left(\text{ran}\left({\beta }_{S_{m-1}}(C_q\mapsto b)\right)\right)\ll {\eta }_{m,b})▹{\sigma }_{m,b})$

An Example

In the following we present, how ${\beta }_{\{B,C,D\}}$ can be constructed based on ${\beta }_{\{B,C\}}$.

The dynamic binding function

With the naming function defined it is surprisingly simple to give the dynamic binding function. To make it even easier we define the function: $\delta :(\text{TYPE}\times \text{TYPE})\to (\text{NAME}\to \text{FEATURE})$

With this function defined we can derive $\gamma$:

$\gamma (S\mapsto f_n)=\{D\mapsto f|\delta (S\mapsto D)\left(f_n\right)=f\}$

What remains is to define $\delta$. As with the naming function we do it recursively. We define ${\delta }_{S_m}$ based on ${\delta }_{S_{m-1}}$ since the following holds:

${\delta }_{S_1}\subseteq {\delta }_{S_2}\subseteq \dots {\delta }_S$

So the definition is:

${\delta }_{S_m}(C_q\mapsto C_p)=\{\begin{array}{ll}\mathrm{\varnothing }& \text{if }q>p\\ {\delta }_{S_{m-1}}(C_q\mapsto C_p)& \text{if }q<=p<m\\ (\text{UNION}b\cdot (b\in {\alpha }_m|{({\delta }_{S_{m-1}}{(b\mapsto b)}^{-1};{\beta }_S(b\mapsto C_m))}^{-1}))\ll {\tau }_m& \text{if }q=p=m\\ \text{UNION}b\cdot (b\in {\alpha }_m|{\beta }_S(C_q\mapsto C_m);{({\delta }_{S_{m-1}}{(C_q\mapsto b)}^{-1};{\beta }_S(C_q\mapsto C_m))}^{-1}\ll {\tau }_m)& \text{otherwise }\end{array}$

An Example

We present the calculation of the function: ${\delta }_{\{B,C,D\}}(B,D)$. Before we can do that we need to calculate ${\delta }_{\{B,C\}}(B,)$