DynBindModel

Author: Matthias Konrad

Related articles:

• Example for the model shown: DynBindModelExamples
• Haskel module that implements the model: DynBindModelHaskell

Motivation:

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

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

Function $\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 construction of the function $\gamma$ is shown, based on any given valid Eiffel system.

There is a special wiki page that shows an example calculation of the dynamic binding function for a complete system: DynBindModelExamples

Notation

This wiki uses the notation introduced in these slides 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). The function operator $\to$ is used for partial functions.

Some operators

We will give some rather informal definitions for the set-theoretic operators used here.

Operator: identity

$\text{id}\left(\{e_1,\dots ,e_n\}\right)=\{e_1\mapsto e_1,\dots ,e_n\mapsto e_n\}$

Operator: inverse

${\{l_1\mapsto r_1,\dots ,l_n\mapsto r_n\}}^{-1}=\{r_1\mapsto l_1,\dots ,r_n\mapsto l_n\}$

Operator: domain

$\text{dom}\left(\{l_1\mapsto r_1,\dots ,l_n\mapsto r_n\}\right)=\{l_1,\dots ,l_n\}$

Operator: range

$\text{ran}\left(\{l_1\mapsto r_1,\dots ,l_n\mapsto r_n\}\right)=\{r_1,\dots ,r_n\}$

Operator: range restriction

$E\mapsto F\in r▹T$ is equivalent to: $E\mapsto F\in r\wedge F\in T$

Example:

$\{1\mapsto 2,2\mapsto 3,3\mapsto 4\}▹\left\{3\right\}=\{2\mapsto 3\}$

Operator: override

$E\mapsto F\in p\ll q$ is equivalent to: $E\mapsto F\in q\vee (E\mapsto F\in p\wedge E\in ̸\text{dom}\left(p\right))$

Example:

$\{1\mapsto 2,2\mapsto 3\}\ll \{1\mapsto 4,3\mapsto 6\}=\{1\mapsto 4,2\mapsto 3,3\mapsto 6\}$

Operator: union

$E\in \text{UNION}x\cdot (x\in S|T)$ is equivalent to: $\mathrm{\exists }x\cdot (x\in S\wedge E\in T)$

Example:

$\text{UNION}x\cdot (x\in \{1,2,3\}|\{x,x^2\})$ is equivalent to: $\{1,2,3,4,9\}$

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 B rename f as f2 redefine f2 select 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 \{B\mapsto \left\{f2\right\}\}\}$

The naming function

The naming function shows for two classes how their feature names are related to each other:

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

In the previous example class C renames feature f to f1. ${\beta }_S(B\mapsto C)\left(f\right)$ thus evaluates to f1. ${\beta }_S(B\mapsto D)\left(f\right)$ evaluates to f2 the selected feature in class D. In this section the naming function of a system is shown:

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

Definition of the naming function

The trivial function $S_0$ is just an empty set. It remains to define $S_m$ for $m>0$ given that we know $S_{m-1}$. This is done by showing what ${\beta }_{S_m}(C_q\mapsto C_p)$ evaluates to for $q\le m$ and $p\le m$. There are two trivial cases. When $q>p$ it evaluates to the empty set and when both $p$ and $q$ are smaller than $m$, it is defined by ${\beta }_{S_{m-1}}(C_q\mapsto C_p)$.

A little more interesting is ${\beta }_{S_m}(C_m\mapsto 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|\text{id}\left(\text{ran}({\beta }_{S_{m-1}}(b\mapsto b)\ll {\eta }_{m,b})\right))& \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})$

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$

The definition:

${\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\\ {\beta }_S(C_q\mapsto C_m);((\text{UNION}b\cdot (b\in {\alpha }_m|{({\beta }_S(b\mapsto b);{\eta }_{m,b})}^{-1};{\delta }_{S_{m-1}}(b\mapsto b)))\ll {\tau }_m)& \text{otherwise}\end{array}$