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

Unfolded forms and replication

The Eiffel ECMA standard defines semantics in two ways. A small core of the language (called CoreEiffel) is described explicitly. The rest is described by giving unfolded forms. These unfolded forms map the constructs that do not belong to CoreEiffel (but to Eiffel) to constructs that do belong to CoreEiffel.

This is especially important for replication. There is an other article that gives an unfolded form for replication. This article shows (somewhat informal) how replication can be reduced away by a similar construct. As a result CoreEiffel does not need any replication anymore.

If replication would be a valid construct of CoreEiffel this would change the very structure of the dynamic binding function $\gamma$ and make it considerably more complex. Its structure would become something like:

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

A model for an Eiffel System

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 }_{\{B,C,D\}}(B\mapsto C)\left(f\right)$ thus evaluates to f1. ${\beta }_{\{B,C,D\}}(B\mapsto D)\left(f\right)$ evaluates to f2, the selected feature in class D. The range of ${\beta }_S$ is a function, this means that every name is mapped to just one name.

As an example the complete function ${\beta }_{\{B,C,D\}}$ is shown:

${\beta }_{\{B,C,D\}}=\{$	$(B\mapsto B)\mapsto \{f\mapsto f\},(B\mapsto C)\mapsto \{f\mapsto f1\},(B\mapsto D)\mapsto \{f\mapsto f2\},$
	$(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 shortcut $S_m$ denotes the system $\{C_1\dots C_m\}$.

A recursive definition of ${\beta }_S$ follows. ${\beta }_{S_m}$ is defined based on ${\beta }_{S_{m-1}}$.

This is sound since: ${\beta }_{\left\{C_1\right\}}\subseteq {\beta }_{\{C_1,C_2\}}\subseteq \dots {\beta }_S$

The trivial function $S_0$ is the empty set. $S_m$ for $m>0$ is defined by 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)$.

${\beta }_{S_m}(C_m\mapsto C_m)$ is an identity function over the set of feature names of $C_m$. The set of feature names consists of the names of

• the inherited features (after renaming).
• the features declared in $C_m$.

The features declared in $C_m$ are given by the domain of ${\tau }_m$. Every base class $b\in {\alpha }_m$ contributes the set: $\text{ran}({\beta }_{S_{m-1}}(b\mapsto b)\ll {\eta }_{m,b})$ to the set of inherited feature names. We can now define:

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

The definition of ${\beta }_{S_m}(C_q\mapsto C_m)$ for $q<m$ depends on two helper functions. Function ${\beta }_S^{\prime }$ ignores whether a features is selected or not, apart from that it is similar to the naming function ${\beta }_S$. Its structure is:

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

The image ${\beta }_{\{B,C,D\}}^{\prime }(B\mapsto C)\left[f\right]$ from the previous example is $\{f1,f2,f3\}$. Its definition is:

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

The second helper function ${\theta }_S$ is again similar to the naming function but it only includes selected feature names. Its structure is:

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

${\theta }_{\{B,C,D\}}(B\mapsto D)$ from the previous example is $\{f\mapsto f2\}$, whereas ${\theta }_{\{B,C,D\}}(C\mapsto D)$ is the empty set. Its definition is:

${\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 definition of ${\beta }_{S_m}(C_q\mapsto C_m)$ for $q<m$ is then:

${\beta }_{S_m}(C_q\mapsto C_m)={\beta }_{S_m}^{\prime }(C_q\mapsto C_m)\ll {\theta }_{S_m}(C_q\mapsto C_m)$

With this we have defined the whole naming function. As a summary we present the whole definition:

${\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}(\text{dom}\left({\tau }_m\right)\cup \text{UNION}b\cdot (b\in {\alpha }_m|\text{ran}({\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})$

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