LogoThe Eiffel Compiler / Interpreter (tecomp)

doc/internals/verify eiffel sw/linked structures

linked structures

Basics of linked structures

The basis of linked structures are linkable elements, e.g.

class C
    f: like  Current   ...
    g: like ?Current   ...
    h: like ?Current   ...

The queries f,g,h, are either attributes or routines. In case of routines they are considered to be very pure, i.e. they shall not have any side effect (not even object creation).

Since f,g,h,... applied to an object x returns an object of the same type as x, they can be applied repeatedly


clearly for g and h only as long as the result is attached to an object.

We define the recursive application

  x.f^0  = x
  x.f^n  = x.f^(n-1).f

These queries have the fixpoint property, i.e. for all objects x (including Void) there exists some non negative integer n such that

  x.f^n = x
  x.g^n = x  or x.g^n = Void
  x.h^n = x  or x.h^n = Void

In other words, repeatedly executing a query like f returns eventually the target and repeatedly executing a query like g or h returns eventually either the target or void.

All these queries define implicitely sequences of objects:

  seq(x,f) = x  x.f  x.f^2  x.f^3 ...  x.f^(n-1)
  seq(x,g) = x  x.g  x.g^2  x.g^3 ...  x.g^(n-1)
  seq(x,h) = x  x.h  x.h^2  x.h^3 ...  x.h^(n-1)

Linkable elements

The above example is not yet very practical, because it defines just sequences of pointers or references.

The thing gets more practical, if we define a class like

    next: ?like Current
    item: G
    seq(x:?like Current): SEQUENCE_FL[G]
       external "builtin"

We can define (similar to above)

   (^0).item = x.item
   (^n).item =^(n-1).next.item
   seq(x,next) = x.item^2.item ...

Now seq(x,next) is a sequence of elements.

It is important to note, that seq(x,next) by being a sequence fulfills the sequence properties outlined in the chapter sequences.

 Local Variables: 
 mode: outline
 coding: iso-latin-1
 outline-regexp: "=\\(=\\)*"
Table of contents

- Basics of linked structures

- Linkable elements