DynBindModel: Difference between revisions

From EiffelStudio: an EiffelSoftware project
Jump to navigation Jump to search
Konradm (talk | contribs)
Konradm (talk | contribs)
Line 112: Line 112:
   \right\},  
   \right\},  
   D \mapsto \left\{  
   D \mapsto \left\{  
      C \mapsto \emptyset,
       B \mapsto \left\{ f \mapsto f2, f \mapsto f3 \right\}
       B \mapsto \left\{ f \mapsto f2, f \mapsto f3 \right\}
   \right\}
   \right\}
Line 118: Line 117:
</math>
</math>
*<math>\alpha = \left\{
*<math>\alpha = \left\{
  B \mapsto \emptyset,
   C \mapsto \left\{ B \right\},
   C \mapsto \left\{ B \right\},
   D \mapsto \left\{ B, C \right\}
   D \mapsto \left\{ B, C \right\}

Revision as of 22:34, 2 October 2006

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:

γ:(TYPE×NAME)→(TYPE→FEATURE)

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:

γ(ANY↦out)

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 {C1,C2…Cn} such that Cq<Cp if 𝐪<𝐩. In practice class C1 will allways be class ANY but this is not of importance here.

The function:

  • τ:TYPE→(NAME→FEATURE)

Yields the features declared in a given class.

  • η:TYPE→(TYPE→(NAME→NAME))

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

η(D)(B) gives the renamings in class D for the inherited class B.

  • α:TYPE→POW(TYPE)

Gives the classes from which a given class inherits:

α(A) Gives the base classes of the of class A.

  • σ:TYPE→(TYPE→POW(NAME))

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

Furthermore we give the following shortcuts:

  • τn for τ(Cn)
  • ηn,b for η(Cn)(b)
  • αn for α(Cn)
  • σn,b for σ(Cn)(b)

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}
  • τ={B↦{f↦B.f},C↦{f1↦C.f1},D↦{f2↦D.f2,f3↦D.f3}}
  • η={C↦{B↦{f↦f1}},D↦{B↦{f↦f2,f↦f3}}}
  • α={C↦{B},D↦{B,C}}
  • σ={D↦{C↦{f1}}}

The naming function

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

Its structure

βS:(TYPE×TYPE)→(NAME→NAME)

As a helper function we also need function:

βS′:(TYPE×TYPE)→(NAME↔NAME)

We will give a recursive definition of βS. Meaning that we will give β{C1,…Cm} given that we already now β{C1,…Cm−1}

This is valid since:

β{C1}⊆β{C1,C2}⊆…βS

Its definition

We introduce the shurtcut Sm to denote the system {C1…Cm}

βSm(Cq↦Cm)={∅if q>mid(dom(τm))∪⋃i=1..∞βSm−1(αm,i,αm,i)≪ηm,iif q=mβSm′(Cq↦Cm)≪(βSm′(Cq↦Cm)▹σm)otherwise 

Where

βSm′(Cq↦Cm)=⋃i=1..∞βSm−1(Cq↦αm,i);(id(ran(βSm−1(Cq↦αm,i)))≪ηm,i)

And:

θSm′(Cq↦Cm)=⋃i=1..∞βSm−1(Cq↦αm,i);(id(ran(βSm−1(Cq↦αm,i)))≪ηm,i)