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 }_{:}(\mathrm{T}\mathrm{Y}\mathrm{P}\mathrm{E}\times \mathrm{N}\mathrm{A}\mathrm{M}\mathrm{E})\to (\mathrm{T}\mathrm{Y}\mathrm{P}\mathrm{E}\to \mathrm{F}\mathrm{E}\mathrm{A}\mathrm{T}\mathrm{U}\mathrm{R}\mathrm{E})$

Relation γ 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 (\mathrm{A}\mathrm{N}\mathrm{Y}\mapsto \mathrm{o}\mathrm{u}\mathrm{t})$

Namely an evaluation of γ with a tuple containing the static type of the call and the name. The result of this is a function. This function will be evaluated at runtime and 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 γ based on any given eiffel system.

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 :\mathrm{T}\mathrm{Y}\mathrm{P}\mathrm{E}\to (\mathrm{N}\mathrm{A}\mathrm{M}\mathrm{E}\to \mathrm{F}\mathrm{E}\mathrm{A}\mathrm{T}\mathrm{U}\mathrm{R}\mathrm{E})$

Yields the features declared in a given class.

• $\eta :\mathrm{T}\mathrm{Y}\mathrm{P}\mathrm{E}\to (\mathbb{\mathbb{N}}\to (\mathrm{N}\mathrm{A}\mathrm{M}\mathrm{E}\to \mathrm{N}\mathrm{A}\mathrm{M}\mathrm{E}))$

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

$\eta \left(A\right)\left(1\right)$ gives the renamings of the first parent part of class A.

We will use the shortcut ${\mathsf{\eta }}_{\mathsf{n},\mathsf{i}}$ for $\eta \left(C_n\right)\left(i\right)$

• $\alpha :\mathrm{T}\mathrm{Y}\mathrm{P}\mathrm{E}\to (\mathbb{\mathbb{N}}\to \mathrm{T}\mathrm{Y}\mathrm{P}\mathrm{E})$

Gives the class from which a given parent part of a class inherits:

$\alpha \left(A\right)\left(1\right)$ Gives the base class of the first parent part of class A.

We will use the shortcut ${\mathsf{\alpha }}_{\mathsf{n},\mathsf{i}}$ for $\alpha \left(C_n\right)\left(i\right)$

• $\sigma :\mathrm{T}\mathrm{Y}\mathrm{P}\mathrm{E}\to \mathrm{P}\mathrm{O}\mathrm{W}\left(\mathrm{N}\mathrm{A}\mathrm{M}\mathrm{E}\right)$

Gives all the selected feature names of a given class.

The naming function

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

Its structure

${\beta }_S:(\mathrm{T}\mathrm{Y}\mathrm{P}\mathrm{E}\times \mathrm{T}\mathrm{Y}\mathrm{P}\mathrm{E})\to (\mathrm{N}\mathrm{A}\mathrm{M}\mathrm{E}\to \mathrm{N}\mathrm{A}\mathrm{M}\mathrm{E})$

As a helper function we also need function:

${{\beta }_S}^{\prime }:(\mathrm{T}\mathrm{Y}\mathrm{P}\mathrm{E}\times \mathrm{T}\mathrm{Y}\mathrm{P}\mathrm{E})\to (\mathrm{N}\mathrm{A}\mathrm{M}\mathrm{E}\leftrightarrow \mathrm{N}\mathrm{A}\mathrm{M}\mathrm{E})$

We will give a recursive definition of ${\mathsf{\beta }}_{\mathsf{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$

${\beta }_{\left\{C_1\right\}}(C_1\mapsto C_1)=\mathrm{i}\mathrm{d}\left(\mathrm{d}\mathrm{o}\mathrm{m}\left({\tau }_{\left\{C_1\right\}}\left(C_1\right)\right)\right)$

We introduce the shurtcut $S_m$ to denote the system with classes $\{C_1\dots C_m\}$

${\beta }_{S_m}(C_p\mapsto C_q)={\beta }_{S_{m-1}}(C_p\mapsto C_q)$ for $p<m\wedge q<m$

${\beta }_{S_m}(C_m\mapsto C_m)=\mathrm{i}\mathrm{d}\left(\mathrm{d}\mathrm{o}\mathrm{m}\left({\tau }_{\left\{C_m\right\}}\left(C_m\right)\right)\right)\cup \bigcup _{i=1..\mathrm{\infty }}{\beta }_{S_{m-1}}({\alpha }_{m,i},{\alpha }_{m,i})\ll {\eta }_{m,i}$

${{\beta }_{S_m}}^{\prime }(C_q\mapsto C_p)=\bigcup _{i=1..\mathrm{\infty }}{\beta }_{S_{m-1}}(C_q\mapsto {\alpha }_{p,i});(\mathrm{i}\mathrm{d}\left(\mathrm{r}\mathrm{a}\mathrm{n}\left({\beta }_{S_{m-1}}(C_q\mapsto {\alpha }_{p,i})\right)\right)\ll {\eta }_{m,i})$

${\beta }_{S_m}(C_q\mapsto C_p)={{\beta }_{S_m}}^{\prime }(C_q\mapsto C_p)\ll ({{\beta }_{S_m}}^{\prime }(C_q\mapsto C_p)▹\sigma \left(C_q\right))$