DynBindModel

Not Ready for Review: This Page is Under Development!

Author: Matthias Konrad

Related articles:

• Haskel module that implements the model: DynBindModelHaskell

Motivation:

Eiffel's 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 described 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.

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

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(q\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

First of all, the model used here does not cover generics. The concepts type and class are thus considered equal.

For making things simpler the following example system is used:

An Eiffel system is basically just a set $S$ of classes (or a set of types). For the example system, $S=\{A,B,D\}$

The features declared in a class

For all these classes there is a partial function that maps the name of the features declared in the class to the actual feature (maybe feature body would have been a better name):

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

For the example system the function is:

$\tau =\{A\mapsto \{f_1\mapsto \underset{\_}{A.f_1},g_1\mapsto \underset{\_}{A.g_1}\},B\mapsto \{f_2\mapsto \underset{\_}{B.f_2},g_2\mapsto \underset{\_}{B.g_2}\},D\mapsto \{f_1\mapsto \underset{\_}{D.f_1},g_1\mapsto \underset{\_}{D.g_1}\}\}$

The direct inheritance function

Eiffel classes can inherit from each other. This is described by the function $\alpha$:

$\alpha :\text{TYPE}\to \mathbb{\mathbb{P}}\left(\text{TYPE}\right)$ For the example system:

$\alpha =\{A\mapsto \mathrm{\varnothing },B\mapsto \left\{A\right\},D\mapsto \{A,B\}\}$

It may surprise, that the functions range is a set of classes and not a list, since it is not reflected how may times a class inherits from a given base class. This is indeed a property of CoreEiffel assumed here but not stated in the standard. This property comes as a result of the unfolded form of replication.

The base classes of class D are expressed as: $\alpha \left(D\right)$

The renaming function

The renaming function yields for every class of the system a second function that describes its renaming. This second function yields for every base class of the class a relation that describes the renaming for a given base class:

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

For the example system it is:

$\eta =\{A\mapsto \mathrm{\varnothing },B\mapsto \{A\mapsto \{f_1\mapsto f_2,g_1\mapsto g_2\}\},D\mapsto \{A\mapsto \mathrm{\varnothing },B\mapsto \mathrm{\varnothing }\}\}$

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

Again, the fact that the final result is not a function but just a relation is surprising. Take it as a property of CoreEiffel, that for a given base class a feature can be renamed to many different names. This is also possible in Eiffel, since it allows several parent parts to refer to the same class.

The select function

The select function yields for a given class the feature names of the features that are explicitly selected for a base class:

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

For the example system:

• $\sigma =\{A\mapsto \mathrm{\varnothing },B\mapsto \{A\mapsto \mathrm{\varnothing }\},D\mapsto \{A\mapsto \left\{g_1\right\},B\mapsto \left\{f_2\right\}\}\}$

No undefine or redefine

Undefine and redefine are not represented in this model. The latter is generally not relevant for the semantics.

This article assumes that there is an unfolded form for undefines which is needed for the join semantics of precondition.

The order

The operator $>$ is the "ancestor of" and $<$ the "descendant of" operator.

For every system there is at least one topological order:

$C:\mathbb{\mathbb{N}}\to \text{TYPE}$

Such that

$\mathrm{\forall }x,y\cdot (x>y\Rightarrow \mathrm{\neg }(C\left(x\right)<C\left(y\right)))$

For the example system there is only one such order:

$C=\{1\mapsto A,2\mapsto B,3\mapsto D\}$

In practice class $C\left(1\right)$ is always class ANY. For simplification, in this article classes are not implicitly inherited by ANY, this simplifies the examples.

Some shortcuts

To simplify the discussion, some shortcuts are introduced:

• $C_n$ for $C\left(n\right)$
• ${\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)$
• $S_m$ for $\{C_1\dots C_m\}$

The full example

The full model of the example is thus:

$S=\{A,B,D\}$

$\tau =\{A\mapsto \{f1\mapsto \underset{\_}{A.f1},g1\mapsto \underset{\_}{A.g1}\},B\mapsto \{f2\mapsto \underset{\_}{B.f2},g2\mapsto \underset{\_}{B.g2}\},D\mapsto \{f1\mapsto \underset{\_}{D.f1},g1\mapsto \underset{\_}{D.g1}\}\}$

$\alpha =\{A\mapsto \mathrm{\varnothing },B\mapsto \left\{A\right\},D\mapsto \{A,B\}\}$

$\eta =\{A\mapsto \mathrm{\varnothing },B\mapsto \{A\mapsto \{f_1\mapsto f_2,g_1\mapsto g_2\}\},D\mapsto \{A\mapsto \mathrm{\varnothing },B\mapsto \mathrm{\varnothing }\}\}$

$\sigma =\{A\mapsto \mathrm{\varnothing },B\mapsto \{A\mapsto \mathrm{\varnothing }\},D\mapsto \{A\mapsto \left\{g_1\right\},B\mapsto \left\{f_2\right\}\}\}$

$C=\{1\mapsto A,2\mapsto B,3\mapsto D\}$

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

When one looks at a feature with name n in a class X and is interested in the name of the selected version of this feature in descendant class Y the naming function tells the answer:

$\beta \left(X\right)\left(Y\right)\left(n\right)$

This function simplifies the construction of the dynamic binding function.

For the example system:

${\beta }_{\{A,B,D\}}=\{$	$(A\mapsto A)\mapsto \{f_1\mapsto f_1,g_1\mapsto g_1\},$
	$(A\mapsto B)\mapsto \{f_1\mapsto f_2,g_1\mapsto g_2\},$
	$(A\mapsto D)\mapsto \{f_1\mapsto f_2,g_1\mapsto g_1\},$
	$(B\mapsto B)\mapsto \{f_2\mapsto f_2,g_2\mapsto g_2\},$
	$(B\mapsto D)\mapsto \{f_2\mapsto f_2,g_2\mapsto g_2\},$
	$(D\mapsto D)\mapsto \{f_1\mapsto f_1,f_2\mapsto f_2,g_1\mapsto g_1,g_2\mapsto g_2\}\}$

Definition of the naming function

The naming function ${\beta }_S$ is defined recursively. Meaning, that ${\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 \subseteq {\beta }_S$

The details of the functions are covered in the succeeding sections, its definition is shown here:

${\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\\ {𝒜}\ll {ℬ}& \text{otherwise }\end{array}$

Where

${𝒜}=\text{UNION}b\cdot (b\in {\alpha }_m|{\varphi }_m(C_q\mapsto b))$

And:

${ℬ}=\text{UNION}b\cdot (b\in {\alpha }_m|{\varphi }_m(C_q\mapsto b)▹{\sigma }_{m,b})$

And:

${\varphi }_m(C_q\mapsto b)={\beta }_{S_{m-1}}(C_q\mapsto b);({\beta }_{S_{m-1}}(b\mapsto b)\ll {\eta }_{m,b})$

The trivial cases

There are two trivial cases:

1. When $q>p$ then according to the definition of the order $C$, $C_q$ is not an ancestor of $C_p$. And thus ${\beta }_{S_{m-1}}(C_q\mapsto C_p)$ evaluates to the empty set in this case.
2. When both $p$ and $q$ are smaller than $m$, it is defined by ${\beta }_{S_{m-1}}(C_q\mapsto C_p)$. Here the recursive structure of the definition can be seen.

The identity function

${\beta }_{S_m}(C_m\mapsto C_m)$ is the identity function over all the feature names of the class $C_m$. It is an identity function since a given feature name in a class has no other name in that same class. The set of feature names of a class $C_m$consists of the names of:

1. The features declared in $C_m$
2. The inherited features (after renaming) of class $C_m$.

The first set is trivial, it is exactly the domain of ${\tau }_m$.

Every base class $b$ of class $C_m$ contributes the set $\text{ran}({\beta }_{S_{m-1}}(b\mapsto b)\ll {\eta }_{m,b})$ to the set of inherited feature names.

The whole identity function is thus:

${\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 helper function

The definition of ${\beta }_{S_m}(C_q\mapsto C_m)$ for $q<m$ is a little harder to construct. Helper function $\varphi$ shown here should simplify things.

There are $|{\alpha }_m|$ paths from class $C_q$ to class $C_m$ that need to be considered. They are shown in the following picture:

${\varphi }_m(C_q\mapsto b)$ describes the naming on the path that goes through $b$:

${\varphi }_m(C_q\mapsto b)={\beta }_{S_{m-1}}(C_q\mapsto b);({\beta }_{S_{m-1}}(b\mapsto b)\ll {\eta }_{m,b})$

The complex case

The union of the helper function over all the base classes $b\in {\alpha }_m$ for given $C_q$ and $C_m$:

${𝒜}=\text{UNION}b\cdot (b\in {\alpha }_m|{\varphi }_m(C_q\mapsto b))$

yields a relation but not a function. The selected features names are not yet taken into account. The explicitly selected features names are:

${ℬ}=\text{UNION}b\cdot (b\in {\alpha }_m|{\varphi }_m(C_q\mapsto b)▹{\sigma }_{m,b})$

So if ${𝒜}$ is overridden with ${ℬ}$ the result is again a function:

${\beta }_{S_m}(C_q\mapsto C_m)={𝒜}\ll {ℬ}$

The dynamic binding function

The initial goal was the definition of the dynamic binding function:

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

For the example system it is defined as:

$\gamma =\{$	$(A\mapsto f_1)\mapsto \{A\mapsto \underset{\_}{A.f_1},B\mapsto \underset{\_}{B.f_2},D\mapsto \underset{\_}{B.f_2}\},$
	$(A\mapsto g_1)\mapsto \{A\mapsto \underset{\_}{A.g_1},B\mapsto \underset{\_}{B.g_2},D\mapsto \underset{\_}{D.g_1}\},$
	$(B\mapsto f_2)\mapsto \{B\mapsto \underset{\_}{B.f_2},D\mapsto \underset{\_}{B.f_2}\},$
	$(B\mapsto g_2)\mapsto \{B\mapsto \underset{\_}{B.g_2},D\mapsto \underset{\_}{B.g_2}\},$
	$(D\mapsto f_1)\mapsto \{D\mapsto \underset{\_}{D.f_1}\},$
	$(D\mapsto g_1)\mapsto \{D\mapsto \underset{\_}{D.g_1}\},$
	$(D\mapsto f_2)\mapsto \{D\mapsto \underset{\_}{B.f_2}\},$
	$(D\mapsto g_2)\mapsto \{D\mapsto \underset{\_}{B.g_2}\}\}$

The definition

With the naming function defined it is surprisingly simple to give the dynamic binding function. To make it even easier the function:

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

is defined. From this function, $\gamma$ can be derived:

$\gamma (ST\mapsto f_n)=\{DT\mapsto \underset{\_}{f}|\delta (ST\mapsto DT)\left(f_n\right)=\underset{\_}{f}\}$

The helper function

What remains is to define $\delta$. As with the naming function it is done recursively. ${\delta }_{S_m}$ can be defined 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}$