SourceForge.net LogoThe Eiffel Compiler / Interpreter (tecomp)

doc/papers/lang/modern eiffel

Definition of "Modern Eiffel"

Introduction

Warning: New version of Modern Eiffel available!!

The following article is the first draft of a description of Modern Eiffel. It has been published in june 2011. In the meantime the definition has been made more precise and changed in some areas significantly. Instead of the following article better read the articles in the thread doc/papers/proof/ to get an up to date description of Modern Eiffel.

Basic motivation for Modern Eiffel and its key features

Along the path in making a compiler for Eiffel which supports concurrency and static verification of assertions some shortcoming of Classic Eiffel have been discovered. In the following a version of Eiffel is described which supports powerful concurrency and static verification of assertions.

The key feature of Modern Eiffel are:

Caveat

The language outline is draft. Some constructs still have to be scrutinized and need more examples and detailed discussion in order to avoid negative effects.

Discussion, critique, ... etc. is strongly encouraged. Feel free to comment at http://sourceforge.net/projects/tecomp/forums.

Grammar

Letter case

Modern Eiffel enforces the letter case which has been the recommended style in classic Eiffel:

Nearly all written Eiffel code respects the style guides. Therefore modern Eiffel just turns the recommended style into a requirement.

Besides the enforced style this rule has the advantage that it opens up new language constructs which would be ambiguous in classic Eiffel. E.g. object creation can be simplified

       create {POINT}.make(x,y)     -- classic form
 
       POINT.make(x,y)              -- new form, 
                                    -- no ambiguity with a feature call
 
       POINT(x,y)                   -- even better, see some other
                                    -- improvements below
 

The goal is not to save keystrokes, the goal is to make the code more readable. The new form is definitely easier to read than the classic form.

Semicolons

Old rule: semicolons are optional (except where they are necessary ;-)).

Style guide: Use semicolons to separate statements or declarations on the same line.

    -- bad style                          -- good style
 
    i:=0  j:=1                            i:=0; j:=1
 
    some_command(a:A b:B)                 some_command(a:A; b:B)
 
    check                                 check
      a=b  -x<y   (z+a)=x                    a=b; -x<y; (z+a)=x
    end                                   end
    --          ^ambiguous -x<y(z+a)
    --      ^ambiguous a=(b-x)
 

New rule: Semicolons are necessary. But in many cases a newline is an implicit semicolon.

A newline is an implicit separator if it appears between a token

  identifier, Result, Current, Precursor, constant, `)', `]'

and a token

  identifier, Result, Current, Precursor, constant, `(', `[',
  `+', `-', free operator, not, old, across, agent

Reason: A new expression can be started with the tokens of the second set.

With that new rule all statements and expressions can be split across many lines in the usual style. The only restriction: An binary operator which is unary and binary (like `+', `-') must be put at the end of the previous line instead at the start of the next line, if used as binary.

 
    -- invalid
    a :=     v1         -- implicit semicolon inserted here
           + v2
           + v3
 
    -- valid
    a :=     v1 +
             v2 +
             v3
 
 

With that definition in some cases commas can be avoided at the end of a line as well

   Semicolon: ";" | Implicit_separator
   Comma:     "," | Implicit_separator

Unfortunately this is not always possible. If the commas separate the items of a list of some entries and the whole list is terminated with a semicolon, the implicit separator can only replace the semicolon but not buth. This implies that in note clauses and multiple assignments all commas must be explicit.

   note
      license: "GPL",   -- comma necessary
               "BSD"    -- semicolon not necessary
      author:  xxx,     -- comma necessary
               yyy
   end
 
 
   x,y := x_expression,   -- comma necesary
          y_expression
 

Annotations

Various syntatic constructs have the possibility of annotations. An annotation is a note clause. Unlike the note clause in classic Eiffel, the note clauses in modern Eiffel can be significant. There are a number of tags which are evaluated by the compiler.

   class
       STATELESS_CLASS
   note
       state: no      -- class has no state, i.e. features can be called
                      -- without a target,
                      -- e.g. STATELESS_CLASS.has_property(some_arg)
   feature
       ...
   end
 
   class SOME_CLASS feature
       some_function: RESULT_TYPE
           note
               state: no         -- this feature does not use the state
                                 -- i.e. it does not use any attribute
                                 -- of the class.
               new_object: no    -- The result is a not a newly created 
                                 -- object (in case of a reference type
                                 -- object).
           do
               ...
           end
   end
 

The annotations allow us to express some properties without introducing new keywords or struggling with the syntax.

Free operators

Free operators are splitted into two classes

The right associative free ops have the additional property that the target appears at the right side of the operator. E.g.

   class SEQUENCE[G] feature
      front_extended alias "+:" (e: G): like Current
         ...
      rear_extended alias "+" (e: G): like Current
      ...
   end
 
   s: SEQUENCE[INT]
   ...
   s := 1 +: 2 +: 3 +: s
 
   -- equivalent to
   s := 1 +: (2 +: (3 +:  s))
 
   -- equivalent to
   s := s.front_extended(3).front_extended(2).front_extended(1)
 
   -- equivalent to
   s := s + 1 + 2 + 3
 
   -- equivalent to
   s := ((s + 1) + 2) + 3
 

Feature names (overloading)

In Modern Eiffel a class can have different features with the same name. The feature name alone does not identify the feature. The feature name together with the signature must be unique. I.e. you can have

  class A feature
      put(x: XT)   ...
      put(y: YT)   ...
      -- requirement: a) XT neither conforms nor converts to YT and vice versa
      --              b) none of them is a formal generic
      ...
  end
 

The feature can be called uniquely as long as there is no conformance or conversion relation between the types in the signature.

This relaxation of the feature name rule requires to address features in the feature adaptation section with signature.

  class  D  inherit 
    A
       redefine
          put(XT)
       end
  end
 

In order to avoid ambiguities with inheritance it is not allowed to inherit a feature from a parent and have another feature with the same name but different signature in the current class. To achieve the intended effect, the inherited feature has to be redefined.

  class  D  inherit 
    A
       redefine
          put             -- there is only one feature named `put' in `A'
       end
  feature
       put(x:XT)          -- the redefined feature
           do 
              Precursor(x) 
           end
 
       put(y:YT)          -- the newly defined feature
           do ... end
  end
 

This mechanism is not strictly necessary. However it enforces the designer of the descendant to decide if he wants to use feature name overloading. Feature name overloading cannot be introduced by accident.

As long as a creation procedures can be identified with the signature only, the name of the creation procedure can be omitted in creation expressions.

   p: POINT
   ...
   p := POINT(x,y)         -- as long as point has only one creation
                           -- procedure with 2 arguments of the corresponding
                           -- types
 
 
   -- if POINT can be created from polar and rectangular coordinates, one of
   -- the creation procedures has to be marked as the default one. For the
   -- other, the longer form has to be used to disambiguate
 
   p := POINT(x,y)
   p := POINT.polar(radius,angle)
 
   -- provided that POINT is defined as
   class POINT create
       rectangular note default: yes end
       polar
   feature {NONE}
       rectangular(x,y:REAL) ...
       polar(x,y:REAL) ....
   end
 

Function declaration

Simple functions which just evaluate an expression `expr' can be declared like e.g.

    divide (i,j:INT) = i/j
 
    -- or with explicit type
    divide (i,j:INT): INT = i/j
 
    -- which is a shorthand for
    divide (i:INT): INT
        require
           j/=0           -- precondition of `/' operator
        do
           Result := i/j
        ensure
           Result = i/j
        end
 
 

Variable declaration (scope, inferred type, etc. )

A variable can be declared within a block. Its scope is the rest of the surrounding block. A surrounding block is either a routine, a branch (if or multibranch statement) or the body of a loop (not the initialization!).

A variable can be initialized at the declaration point and its type can be inferred from the type of the expression.

Examples:

    some_routine (a, b: INTEGER)
       do
          local i: INTEGER
          local j: INTEGER := a + b   -- with explicit initialization
          local k := a - b            -- inferred type
 
          ...
          from
             local l := 0
          until
             l = max_value or else cond
          loop
             local x = some_exp      -- x cannot be reassigned!!
             l := l + 1
          end
          -- x no longer valid outside the body
 
          if l = max_value          -- l still valid here
          then
             ...
          else
              local (a := aexp; b := bexp)  -- block of variables
                                            -- valid in the else branch only
              ...
              local i := a + l              -- shadows the outer block variable
              ...
          end
       end
 

Advantage: Declaration, initialization and use can be made in a very limited scope. This enhances readability. In classic Eiffel it has often be a problem that the use and the declaration of local variables are far apart. At first sight it was in many cases not easy to find out, if an entity is a local variable or argument of the enclosing routine or an attribute of the enclosing class. The (ugly) workaround has been to prefix all arguments with `a_' and all local variables with `l_'.

Local routines

In modern Eiffel it is possible to declare local routines within a block.

   class C feature
       some_routine
           do
              ...
              from var idx:=0 until idx=100 loop
                 local inc(i:INTEGER) = i+1
                 ...
                 idx := inc(idx)                 
              end
           end
 

Note that local routines are closures. They have access to all data accessible in the surrounding blocks of their definition point.

The following example which calculates the square root of a real number by Newtons method iteratively demonstrates the point (example taken from Odersky: "scala by example").

     sqrt (c: FLOAT): FLOAT
         require
             c >= 0
         do
             local (
                 is_good_enough (guess: FLOAT): BOOLEAN =
                        (c - guess.squared).abs <= 0.0001
 
                 improved(guess: FLOAT): FLOAT =
                        (guess + c / guess) / 2
 
                 sqrt_iter(guess: FLOAT): FLOAT =
                        if is_good_enough(guess) then 
                           guess
                        else  
                           sqrt_iter(improved(guess))
                        end
             )
             Result := sqrt_iter(1.0)
         end
 

This example demonstrates the use of `if' expressions as well.

For those interested in the question "Why does the algorithm work?" some elementary math.

Calculating the square root of a number `c' is solving the equation `c-x.squared=0'. Instead of calculating the zero of `c-x.squared' we calculate the zero of the tangent of `c-x.squared' at some initial guess `g'. That zero we take as a new guess and iterate until the precision is good enough.

     equation to solve:  c - x.squared = 0
     an initial guess:   g  with probably (c-g.squared) /= 0
     tangent at g:       (c-g.squared) - 2 * g * (x-g)
     zero of the tangent: x = (g + c/g) / 2
     
     the zero of the tangent is taken as an improved guess

Multiple assignment

Modern Eiffel supports multiple assignment.

 
    x,y,z,... := xexp, yexp, zexp, ....
 
    -- semantic: first evaluate all xexp, yexp, ... and then do 
    --           all assignments
 
 
    x,y := y,x       -- swaps `x' and `y'
 
 

Tuples can be decomposed by a similar construct.

 
    t: TUPLE[XT,YT]
    x: XT
    y: YT
 
    ...
 
 
    [x,y] := t
 
    local [a,b] := t       -- also for newly created locals possible
 
    [_,y] := t             -- first component discarded
 

Output arguments

In Eiffel we have command query separation, i.e. a query should not change anything (asking a question should not change the answer). Modern Eiffel enforces this. Therefore it is no longer possible to write a routine which has a side effect and returns a result. This is needed to ensure that assertions do not have side effects and for the verification of the software (see chapter about software verification).

However it is often convenient to have the possibility to do something and return a value. Examples:

For the stack the operation can be split. There is a feature `item' returning the top element and a feature `remove' which removes the top element.

The same can be done for io, but this blows up the io class with many attributes (e.g. like `last_character', `last_string', `last_integer', `last_real', `last_natural', ...).

Modern Eiffel introduces output arguments of procedures. A procedure with output arguments is declared as

  class FILE feature
       read_character -> c:CHARACTER
           do
              ...  -- the body must assign to `c'
              ...
           end
  end
 

and used as

   f: FILE
   ...
 
   -- output to an already declared entity (variable or attribute)
   f.read_character ->  c
 
   -- output used to initialize a new local variable
   f.read_integer -> local i
 

The general case is

  -- declaration
  class C feature
      r(a1:A1; a2:A2; ...) -> r1:R1; r2:R2; ... 
          do  ... end
  end
 
  -- usage
  c: C
  ...
  c.r(a1,a2,...) -> r1,r2,...
 

Moreover if the declared procedure does not have input arguments the `->' token can be used as an alias. This is convenient in case of of io.

  class FILE feature
       read_character alias "->" -> c:CHARACTER
           do ... end
 
       read_integer alias "->" -> i:INTEGER
           do ... end
 
       ...
  end
 
 
  f: FILE; c:CHARACTER; i:INTEGER
  ...
  f -> c         -- calls f.read_character
  f -> i         -- calls f.read_integer
 
  -- or use as a shorthand
  f -> c -> i
 
  -- newly created local variables can be used as well, however in that case
  -- the type has to be provided in order to resolve ambiguities
  f -> local c:CHARACTER ->  local i:INTEGER
 

Generic routines

Like classes, routines can have formal generics as well.

  -- declaration
  class SEQUENCE[G] feature
      zipped [H] (other: SEQUENCE[H]):  SEQUENCE[TUPLE[G,H]]
            -- Sequence with tuples where the first element is of `Current'
            -- and the second element is the corresponding element
            -- of `other'
         require
            count = other.count
         do
            ...
         end         
  end
 
  -- usage
  local ( s1 = SEQUENCE(1,2,3)
          s2 = SEQUENCE('a','b','c') )
 
  s3 := s1.zipped[CHARACTER](s2)
 
   -- in that case the actual generic can be inferred
  s3 := s1.zipped(s2)
 
  check
     s3 = SEQUENCE([1,'a'], [2,'b'], [3,'c'])  -- equality see below
  end
 

Types and objects

Equality

The equality operator `=' always returns object equality i.e. `a=b' compares the objects represented by `a' and `b' and not the references to the objects.

The equality operator can nearly always be considered as an alias for the function `is_equal'. There is one exception with detachable types (see below: void safety). I.e. the compiler does not let you compare objects by `=' if their types are not compatible.

The class OBJECT has a standard definition of `is_equal'. The standard `is_equal' compares objects deeply. All references are followed during the comparison of two objects by `='. The feature `is_equal' can be redefined in descendants.

In order to express reference equality, Modern Eiffel has the class ID[G] with the following outline:

   class
       ID[G:ANY]
   create
       make
   convert
       make( {ANY} )
   feature {NONE}
       make (e: G)    
           external "built_in"
           ensure
               ID(item) = ID(e)
           end
    feature
       item: G
    end
 
    -- usage of the ID class --
    a,b,c: STRING
 
    a := "Hello world\n"
 
    b := a
    c := a.twin
    check
       a = b
       a = c
       ID(a) =  ID(b)
       ID(a) /= ID(c)
    end
 

The designer of a class can specify the equality relation via redefinition of `is_equal'. But the relation defined by `is_equal' must be an equality relation. The class OBJECT specifies the equality relation:

  class OBJECT ... invariant
 
     reflexive:    all(x: like Current): x = x
 
     symmetry:     all(x,y: like Current): x = y => y = x
 
     transitivity: all(x,y,z: like Current):
                       require
                          x = y
                          y = z
                       then
                          x = z
                       end
  end
 

See chapter verification for explanation of `all' and `require...then...end''.

Beside equality Modern Eiffel has the notion of `copy equality'. Copy equality is stronger than (or as strong as) equality and is by default defined as flat equality. Two objects are copy equal if their attributes are one by one identical. This form of equality is very useful for containers where usually two containers are copy equal if they contain indentical elements (and not only equal elements).

In order to define copy equality the class OBJECT has the feature `is_copy(o:like Current):BOOLEAN' with the alias `=='. The designer of a class can redefine `is_copy' in order to achieve a behaviour different from the default definition. However `is_copy' must still be stronger than `is_equal' and define an equivalence relation.

In order to express that two objects `a' and `b' are identical (i.e. ID(a)=ID(b)) Modern Eiffel has the shorthand `a===b'.

      a = b       -- objects `a' and `b' are equal (default: deep equal)
 
      a == b      -- objects `a' and `b' are copy equal (default: flat equal)
 
      a === b     -- objects `a' and `b' are identical
 

All three equalitiy operators are

Hashable

All objects in Modern Eiffel are hashable. All the basic types (INT, NAT, ARRAY, BOOLEAN, ...) have a builtin hash function.

For user defined composite types a builin hash function calculates a combined hash based on the hashes of all recursively reachable basic types objects. The class OBJECT has a feature named `hash_code' which calculates the hash.

The designer of a class can redefine OBJECTs hash. But the redefinition of hashes must be consistent with equality. Equal objects must return equal hash codes.

  class OBJECT ... invariant
     ...
     hash: all(x,y: like Current):  x = y  => x.hash_code = y.hash_code     
  end
 

Immutability

Modern Eiffel introduces readonly and immutable types. Any type `T' can be prefixed with `readonly' or `immutable'.

   x: immutable T       all objects attached to `x' are immutable, i.e. not
                        command can be called on x, only queries
                        the immutability is deep, i.e. `x' only returns
                        `immutable's
   x: readonly T        like immutable, but other variables may refer to the
                        same object in a mutable way. The object can change,
                        but not via `x' or any other variable to which `x'
                        passes the object
   `T' converts to  `immutable T':   conversion creates a deep clone
   `immutable T' converts to `T':    conversion creates a deep clone
   `readonly T' converts to `T':     conversion creates a deep clone
   `T' conforms to  `readonly T'
   `immutable T' conforms to `readonly T'

It is possible to declare a class as immutable. Classes declared immutable don't have any commands and their queries return only immutable type objects.

All basic classes like INT, CHARACTER, STRING etc are immutable, i.e. declared as

   immutable class 
      STRING
   feature
      ...                 -- only queries, except the creation procedures
   end
 

It is possible to inherit from an immutable type which is derived from a mutable type

   class
       C
   inherit
       immutable B         -- inherit only the queries of `B' which return
                           -- only immutable types
   feature
       ...                 -- C can have commands, if not declared as
                           -- immutable; but the commands cannot modify
                           -- or reattach attributes of B
   end
 

Generic types can have two stages of immutability

   immutable SEQUENCE[T]   -- immutable sequence, but elements can be modified
 
   immutable SEQUENCE[immutable T]   -- neither the sequence nor the elements
                                     -- can be modified
 

The same applies to `readonly'.

Type safety

The basics

Modern Eiffel is completely type safe. Type safety means that if you have an entity of type T (i.e. static type T), you can call all features of T according to the feature declarations in T without any risk of a runtime type error. I.e. you don't need to think which objects might be attached to that entity at runtime. Sometimes type safety is expressed as

   A type is always what it pretends to be!

Classic Eiffel is not type safe according to this definition because it allows catcalls (cat: changing availability or type) which can cause runtime errors and cannot be detected at compile time.

In order to achieve the goal of type safety, modern Eiffel does not allow conformance and covariant redefinitions of arguments in the same inheritance relation . Modern Eiffel has two different subtyping possibilities:

The class

  class
     C
  inherit
     -> A
     B
  ...
  end
 

is a conformant descendant/subtype of type A and only a normal subtype of type B with the following consequences

  local (a: A; b: B; c:C)
 
  a := c         -- allowed
  b := c         -- compile time error: "C does not conform to B"
 

Default inheritance

If a class has no inheritance clause (neither conformant nor normal) the implicit inheritance clause is

  class
     C
  inherit 
     -> ANY
     OBJECT
  ...
  end
 

where the classes ANY and OBJECT are defined as

  class ANY feature
     type: TYPE
     out:  STRING
  end
 
  class
     OBJECT   -- implicitely inherit -> ANY
  feature
     is_equal(other: like Current): BOOLEAN
     is_copy (other: like Current): BOOLEAN
     twin: like Current
  end
 

The implicit inheritance clauses can be overridden. E.g. we can define

  class
     D
  inherit
     ANY
  end
 

which defines a class D which has no equality features. The universal conformance principle is valid since all types conform to ANY.

Covariant redefinitions of arguments

Normal inheritance allows implicit covariant redefinitions of arguments. Arguments are implicitly redefined if they are anchored (like Current or like feature). E.g. the argument `other' of the feature

   is_equal(other: like Current): BOOLEAN
 

is implicitely redefined in each descendant to the type of the descendant. All classes which inherit (normally) from OBJECT have a feature `is_equal' which needs an argument of the same type. But due to normal inheritance from OBJECT (as default), there is no conformant inheritance from OBJECT.

As soon as a class C decides to inherit conformant from type A (i.e. `inherit -> A') all features which have anchored arguments in A are deanchored and are inherited in its deanchored form in C. Even if class C decides to redefine an anchor (i.e. redefine the result of a query covariantly) all arguments anchored to that query in the parent A get deanchored and are not affected by the redefinition of the anchor (which is no longer an anchor!!).

A class C might want to inherit conformant from OBJECT. In that case the feature `is_equal' of class C has the signature

   is_equal(other: OBJECT): BOOLEAN
 

i.e. all objects of class C can be compared by `is_equal' with all other objects of classes which have decided to inherit conformant from OBJECT as well.

All conformant descendants of a certain class A share all public features of A with exactly the same signatures in its arguments.

The full modelling power of covariant redefinitions with normal inheritance is kept. It is possible to design ROOMs accepting PERSONs to sleep in it and BOY_ROOMs acception only BOYs and GIRL_ROOMs accepting only GIRLs (in order to keep the parents happy).

Generic constraints

Generic constraints can be based on conformant or normal inheritance. E.g. class CG

   class CG[G1->A, G2:B] ... end
 

expects all actual generics fed into G1 to conform to A and all actual generics fed into G2 to inherit normally from B.

Covariant redefinitions are restricted to implicit redefinitions with anchored types only. This restriction is necessary to make generic classes typesafe. A class CG[G1->A, G2:B] accepts actual generics for G2 which inherit (at least normally) from B. Since arguments can only be redefined in the descendants of B if they are anchored, the compiler is able to check at compile time that CG uses all features of G2 in a safe manner.

If descendants of B were allowed to redefine arguments to arbitrary subtypes of the arguments declared in B, the compiler would have no chance to verify the validity of the code of CG without knowing the actual generics which will be fed into the formal generic G2.

Multiple constraints are annotated in a similar manner

   class CG[G: {->A, B}]  ... end
 

The default generic constraint is

   class CG[G:{->ANY,OBJECT}] ... end
 

No generic conformance!

There is no conformance of generic types based on actual generics. I.e. ARRAY[RECTANGLE] does not conform to ARRAY[SHAPE] even if RECTANGLE conforms to SHAPE. The reason is simple. Suppose you have a graphics library with RECTANGLEs, CIRCLEs, ELLIPSEs which all conform to SHAPE. Then you define an array of rectangles and put some rectangles into the array. If the array of rectangles conformed to an array of shapes you could attach the array of rectangles to an array of shapes and insert into it circles and ellipses screwing up your object which is in reality an array of rectangles.

If you want to have an array of shapes, then declare it ARRAY[SHAPE] and you can insert arbitrary shapes. If you want an array of rectangles the compiler makes sure that you only insert rectangles.

Universal conformance

All type conform to ANY. Therefore all attachments of the form

   local (a:ANY; s:S; t:T)
   ...
   a := s
   a := t
 

are possible. But ANY has no equality features. Therefore it is not possible define the type ARRAY[ANY], since ARRAY has the class header class ARRAY[G] which is equivalent to class ARRAY[G:{->ANY,OBJECT}] and ANY does not inherit normally from OBJECT. The best approximation for ARRAY[ANY] is ARRAY[ID[ANY]].

Void safety

Void safety belongs to type safety. An expression having type T must return an object of type T. It is not allowed that it returns no object or `Void'. Modern Eiffel ensures this by checking that all variables (locals or attributes) are initialized properly before its use.

But sometimes (e.g. in linked structures) it must be possible that an attribute is `Void' i.e. it is not attached to any object. If the SW designer wants this possibility, he has to declare the attribute as `detachable T'.

On any expression of type `detachable T' no features can be called, because the expression could return `Void'. In order to get the object possibly attached to an expression of type `detachable T' an object test has to be made

    exp: detachable T
    ...
 
    if attached exp as t then
       t.some_feature(arg)
    else
       t.some_feature(arg)  -- invalid, t used outside its scope!!!
    end
 
    t.some_feature(arg)     -- invalid, t used outside its scope!!!
 

The following explains the different possible object tests:

   attached exp
       -- boolean expression returning True if the expression returns
       -- a real object (i.e. not Void)
 
   attached exp as t
       -- the same boolean expression with the side effect of
       -- attaching the object to a new local variable `t' of type T
 
 
   attached {DT} exp
       -- returns True, if the expression returns an object of type
       -- DT (must be a descendant of type T)
 
   attached {DT} exp as t
       -- the same with a side effect of attaching the object
       -- to a new local variable `t'
 

The newly created local variable is valid in a scope, where the object test is guaranteed to have been positive (i.e. the corresponding if branch).

The object test is the method of choice, if an expression can return an object or void. If it is already known that an object is attached to an expression (this is an assertion which the SW designer makes), the type of the expression can be casted from `detachable T' to `T' via

   exp: detachable T
   ...
   exp.attached.some_feature(arg)
   --           ^ call a feature on that object
   --  ^ assertion that exp returns an object 
 
 
   exp.attached{DT}.some_feature(arg)
   --               ^ call a feature on that object
   --  ^ assertion that exp returns an object of type DT
 

The `attached' assertions can either be proved statically by the compiler or at runtime. In case that the assertion is not valid at runtime, an exception is raised.

The usage of the `attached' assertion can be seen in the example of a linked list.

  class LINKABLE[G]  feature
      item: G
      next: detachable like Current
      put_next (o: detachable like Current) ...
  end
 
  class LINKED_LIST[G]
  feature {NONE}
     first_cell: detachable LINKABLE[G]
  feature
     is_empty: BOOLEAN = (first_cell = Void)
 
     first: G
         require 
            not is_empty
         do
            Result := first_cell.attached.item
         end
     ...
   end
 

Local types

Modern Eiffel has local types. There are two forms of local types

  deferred class C feature
     T1 = SOME_TYPE
     T2: BASE_TYPE
  end
 

In the first case T1 is defined. It can be redefined in descendants to any subtype of SOME_TYPE. T2 is deferred. It must be effected in effective descendants to any subtype of BASE_TYPE.

An abstract class OBSERVER can observe subjects and receive updates from these subjects.

  deferred class OBSERVER feature
     SUB: SUBJECT
     update_with(s: like SUB)  deferred end
  end
 

The companion subject class has the definition

  deferred class SUBJECT feature
     OBS: OBSERVER
  feature{NONE}
     observers: SEQUENCE[like OBS]
  feature
     register(o:like OBS)
        do
           observers.extend_rear(o)
        ensure
           has_observer(o)
        end
     notify
        do
           across observers as o loop o.update_with(Current) end
        end
  end
 

Both classes have an abstract type which can be any subtype of SUBJECT or OBSERVER respectively. Effective descendants have to effect the abstract types with concrete ones. We define a SENSOR which inherits from SUBJECT and a DISPLAY which inherits from OBSERVER.

  class SENSOR inherit SUBJECT
  feature
     OBS = DISPLAY    -- effecting of OBS
     label: STRING
     value: FLOAT
     change_value(v: FLOAT)
        do
           value := v
           notify
        end
  end
 
  class DISPLAY inherit OBSERVER feature
     SUB = SENSOR     -- effecting of SUB
     update_with(sub: like SUB)
        do
           print(s.label + " has value " + s.value.out + "\n")
        end
  end
 

Descendants of SENSOR and DISPLAY can redefine OBS and SUB. But the redefinition must be a subtype of DISPLAY and SENSOR respectively.

With local types it is possible to define a family of abstract classes which can have covariant redefinitions in their descendants. Local types are similar to anchored types of the form like other_feature of ISE Eiffel but are more flexible. Note that neither SUBJECT has a query of type OBSERVER nor does OBSERVER have a query with the type SUBJECT to use as an anchor. Therefore the above pattern would not be expressible in ISE Eiffel.

Family polymorphisms

With local types it is possible to express family polymorphisms. The exprssible family polymorphisms can be a runtime polymorphisms.

The basic problem:

Polymorphism (i.e. conformant inheritance) allows us to define a base class CB with feature f. Then we can define conformant descendants C1, C2, ... which redefine the feature. If x is of static type CB and is attached to an object of type Ci, we can safely call "x.f". The type system of Eiffel ensures that all conformant descendants of CB have a feature "f". The caller of "x.f" does not depend on the actual runtime object attached to x.

Now lets say we have two base classes A_BASE and B_BASE which are deferred. This two classes might be related. I.e. A_BASE might have attributes of type B_BASE (i.e. A_BASE is a client of B_BASE) or the other way round or in both directions. Now we create descendants A1,B1,A2,B2,... and we always want the Ai and Bi are related in the above sense but not Ai with an arbitrary Bj (i/=j). E.g. A_BASE might have a feature f(b:B_BASE) and if x and y are of static type A_BASE, B_BASE we want to be sure that the feature call "x.f(y)" is type safe. Unfortunately this is not the case if the Ais redefine that argument of "f" covariantly (therefore Modern Eiffel does not allow covariant redefintion of afrguments under conformant inheritance).

But with local types the following is possible

  deferred class 
     A_BASE 
  feature
     B -> B_BASE     -- B can be any conformant descendant of B_BASE
 
     some_b: B       deferred end
     f(a: B)         deferred  end
  end
 
  deferred class B_BASE feature ... end
 
  class
    A1
  inherit
    -> A_BASE
  feature
    B = B1
    some_b: B   do ... end
    f(a:B)      do ... end
  end
 
  class B1 inherit -> B_BASE feature ... end
 
 
  -- now the following routine is typesafe
  do_something(a: A_BASE;  b: a.B)
     do
        a.f(b)
     end
 
  -- and can be called e.g. like
  readonly a: A_BASE
  ...
  do_something(a, a.some_b)
 

The type "a.B" is called a dependent type. It is important that the entity "a" (local variable, argument or attribute) cannot be reattached. Arguments can never be reattached, attributes and local variables can be declared as "readonly" (i.e. not reattachble). It is important to distinguish the cases that an entity is readonly (i.e. cannot be reattached) or that an object is readonly (i.e. cannot be changed). An object attached to a readonly entity can be changed. It is just the entity which cannot be reattached.

Kernel library

Since Modern Eiffel does not try to be backward compatible with Classic Eiffel, the class names in the kernel library can be cleaned up.

    -- Classic Eiffel --                --  Modern Eiffel --
    ANY                                 ANY, OBJECT
    CHARACTER, CHARACTER_8/32           CHARACTER, CHARACTER_8/32
    NUMERIC                             NUMERIC
    INTEGER, INTEGER_8/16/32/64         INT, INT_8/16/32/64
    NATURAL, NATURAL_8/16/32/64         NAT, NAT_8/16/32/64
                                        INTEGER        -- arbitrary sized
                                        NATURAL        -- arbitrary sized
    REAL, REAL_32/64                    FLOAT, FLOAT_32/64
    COMPARABLE                          ORDERED
    PART_COMPARABLE                     PARTIALLY_ORDERED
    HASHABLE                            -- no longer necessary
    STRING                              STRING        -- immutable
                                        STRING_BUFFER -- mutable
    SPECIAL[G]                          ARRAY[G]
    ARRAY[G]                            -- no longer necessary
                                        SEQUENCE[G]   -- like a C++ vector
                                        ID[G]
 

Reason:

Functions and Routines as objects (agents)

Function objects

If we have a function

   squared(x:INT): INT = x*x
 

we can create a function object by `agent squared'. The function object is of type `INT->INT' and can be passed around like any other object. Application of the function is done via the bracket alias.

   local fobj: INT->INT := agent squared
 
   -- or with the type inferred
 
   local fobj  := agent squared
 
   local i := fobj[2]   -- attaches `4' to `i'
 

It is possible to create an anonymous function object by

   local fobj:= agent(x:INT):INT = x*x
 

Function objects are closures. They can access all data which are accessible in their creation context. The data of the context are stored within the function object because the function object can be called in a context where the data are no longer available.

   local inc: INT->INT
 
   if some_condition then
      local i
      ...
      inc := agent(x:INT):INT = i+x
   end
 
   -- value of variable `i' is no longer available
 
   local z := 0
   z := inc[z]   -- z incremented by the value of `i' within the context where
                 -- the function object `inc' has been created.
 

The type (A,B,..)->T is expanded to FUNCTION[A,B,...,T]. Like class TUPLE the class FUNCTION is a generic class with a variable number of generic paramenters.

    class FUNCTION feature
       item alias "[]" (?): ?      -- signature depends on the actual generics
           require
               defined_at(?)
           external 
               "built_in"
           end
 
       defined_at (?): BOOLEAN
           external "built_in"
           end
    end
 

General syntax

a) type declarations:

   INT -> INT        -- function object taking an INT and returning an INT
 
   (INT,STRING)->INT -- function object taking an INT and a STRING and
                     -- returning an INT
 
   agent(INT,STRING):INT  -- the same with the `agent' keyword
 
   agent(STRING)     -- procedure object taking a STRING
 
 

b) function/procedure object creation

   -- suppose we have the features f(a:A;b:B):R and p(a:A;b:B) within 
   -- the current class
 
   agent p(?,expb)  -- create a procedure object which takes an A,
                    -- the value of `expb' is stored within the procedure object
 
   agent f(?,?)     -- create a function object taking A,B and returning R
 
   agent f(exp,?)   -- create a function object taking B and returning R
                    -- value of `exp' is stored within the function object
 
   agent f          -- the same as `agent f(?,?)'
 
   a = ?            -- create a function object which stores `a' and takes an
                    -- argument of the same type and returns a BOOLEAN
 
   i <= ?           -- create a function object which stores `i' and takes an
                    -- argument of the same type and returns a BOOLEAN
 
   -- like `i<=?', but more explicit
   agent(x:INT):BOOLEAN = i <= x
 
   -- create a function object which stores `y' and `z' from the creation 
   -- context and takes an INT and returns a BOOLEAN
   agent(x:INT):BOOLEAN
       require
          x /= 0
       do
          Result := y/x <= z
       ensure
          Result = (y/x) <= z
       end
 
   -- short form
   y/? <= z        -- provided that the type of `?' can be inferred unambigously
 

c) function/procedure object execution

    x := fobj[a,b]   -- calculate the result of the function object `fobj'
                     -- with arguments `a' and `b' and attach the result to `x'
 
    pobj[a,b,c]      -- execute procedure of the procedure object `pobj'
                     -- with the arguments `a', `b' and `c'.
 

Currying

Functions can return functions. Modern Eiffel has a special syntax for that

    sum(f:INT->INT)(a,b:INT):INT =
        if a>b then 0 else f[a]+sum(f)[a,b] end
 
 
    -- is a shorthand for
 
    sum(f:INT->INT): (INT,INT)->INT
       do
          local sum_f(a,b:INT):INT = if a>b then 0 else f[a]+sum_f(a+1,b) end
          Result := agent sum_f
       end
 

Scalability

Small programs

Scripting

Clusters and libraries

Class name rules

Compiled libraries

Verification

Basics

Modern Eiffel can verify assertions at compile time. It has a proof engine which can do that in many cases automatically. I.e. the proof engine includes a simple theorem prover. Since proving of theorems (in the Eiffel case `assertions') is undecidable, the proof engine cannot verify all assertions.

In case that the proof engine reports an assertion as unprovable, the assertion is either wrong or needs some additional assertions or needs some proof from the SW designer.

In order to specify proofs manually Modern Eiffel has some proof language which allows the designer to specify the proof idea (if needed) and the proof engine verifies that the proof is correct and does the simple steps automatically.

Fortunately -- well written assertions assumed -- many assertions can be proved automatically by the proof engine.

Command query separation

Modern Eiffel in verification mode enforces strict command query separation. A query must not have any (visible) side effects. A query can modify private attributes. But the result of all queries must not depend on the value of these modified private attributes.

Full specification

Commands can modify the state of the target object and the state of the arguments. It is necessary to specify all changes which a command makes.

   class SEQUENCE[G] feature
       extend_rear(e:G)
              -- Add the `e' to the end of the sequence
          require
             is_extendible
          do
             ...
          ensure
             Current == old rear_extended(e)
          end
 
       rear_extended alias "+" (e: G): like Current
              -- The current sequence with `e' appended at the end.
           require
              is_extendible
           do
              ...
           ensure
              Result.count        =   count + 1
              ID(Result.last)     =   ID(e)
              Result.last_removed ==  Current  
           end
   end
 

Modern Eiffel does not allow any modifications which are not specified in the postcondition. The above command `extend_rear' modifies the current object in a manner that the modified object is a copy of the old object `rear_extended' with `e'. The specification says implicitely that the object attached to `e' is not modified. The "closed world assumption" is valid. Anything not specified must not change.

A postcondition is binding for all conformant descendants. A conformant descendant must not make more visible modifications than specified in the ancestor. This allows the proof engine to apply local reasoning.

Note: A conformant descendant can make postconditions stronger (e.g. guarantee identity or copy equality instead of equality). But it must not modify more than the ancestor has specified.

Quantified expressions

Modern Eiffel introduces quantified expressions in assertions. These are best explained by example

    all(i:INT): 0<=i and i<count => item(i)/=e
       -- all item(i) in the range 0<=i and i<count are not equal to e
 
    -- or using syntactic sugar for implications
    all(i:INT):
         require
             0 <= i
             i <  count
         ensure
             item(i)/=e
         end
 
    some(i:INT): 0<=i and i<count and then item(i)=e
       -- there exists an item(i) in the range 0<=i and i<count which is equal
       -- to e
 
    -- with the obvious de Morgan rules
    not (some(a:A): prop(a)) = (all(a:A):  not prop(a))
    not (all(a:A):  prop(a)) = (some(a:A): not prop(a))
 

The postcondition of `rear_extended' can be described with quanitified expressions as well.

       rear_extended alias "+" (e: readonly G): like Current
              -- The current sequence with `e' appended at the end.
           require
              is_extendible
           do
              ...
           ensure
              Result.count        =   count + 1
              ID(Result.last)     =   ID(e)
              Result.last_removed ==  Current  
              all(i:INT): 0<=i and i<count => Result[i]===item(i)
           end
 

Construction of proof trees

An assertion is proved by constructing a proof tree. On the top of the proof tree is the assertion to be proved and the childs of the node are assertions which together imply the parent assertion. The leave of a proof tree are other already assertions which are valid in the context.

The proof engine is able to construct a lot of proof trees automatically. Suppose we want to prove

  0 <= x + 1
 

in a context where we have the available other assertions

   0 <= x
   x < count
   all(a,b,c:INT)
        check
            a < b           => a < a+1
            a <=b and b<=c  => a <= c
            a < b           => a <= b
        end
 

Given these assertions the prove engine can construct the proof tree

   0 <= x+1
   from
       -- apply transitivity law
       0 <= x        -- true by context
       x <= x+1
       from
          -- apply "less than => less equal"
          x < x+1
          from
             -- apply "no overflow as long there is a bigger"
             x < count    -- true by context
          end
       end
   end
 

The prove engine can construct all prove trees in which the expression depth of the child nodes never exceed the expression depth of the parent node. This restriction is necessary to guarantee termination.

Even with that restriction the proof engine can proof a lot of assertions. As a more complicated example let us see how the proof engine verifies the quantified expression

   all(i:INT): 0<=i and i<x+1 => item(i)/=e
 

in a context like

   0<=x
   x<=count
   x<count
   item(x)/=e
   all(i:INT): 0<=i and i<x => item(i)/=e
 
   -- general assertions
   all(a,b:INT; p,q,r:BOOLEAN) 
   check
       r1: b<b+1 => a<b+1 = (a<b or a=b)
       r2: a < b => a<a+1
       r3: (p and (q or r)) =  (p and q or p and r)
       r4: (p or q => r)    =  (p => r and q => r)
   end
 

The proof tree looks like

   all(i:INT): 0<=i and i<x+1 => item(i)/=e
   from
       -- apply rule r1
       x < x + 1
       from
          -- apply rule r2
          x < count
       end
       all(i:INT): 0<=i and (i<x or i=x) => item(i)/=e
       from
          -- apply rule r3
          all(i:INT): 0<=i and i<x or 0<=i and i=x) => item(i)/=e
          from
             -- apply rule r4
             all(i:INT) check
                 0<=i and i<x => item(i)/=e  -- true by context
                 0<=i and i=x => item(i)/=e
                 from
                     -- prove an implication by proving the consequent with
                     -- the help of the antecedent
                     require
                        0<=i
                        r5: i=x
                     ensure
                        item(i)/=e 
                        from
                            -- apply rule r5
                            item(x)/=e  -- true by context
                        end
                     end
                 end
             end
          end
       end
   end
 

Note that none of the expression gets more complicated than the expression of the corresponding parent node. Therefore the proof engine can construct the tree automatically.

Example: class ACCOUNT

The basic idea can be demonstrated by a class ACCOUNT which models a bank account. You can deposit and withdraw money. The class doesn't let you withdraw more money than there is in the account, i.e. the balance must be always not negative.

Furthermore the account keeps track of all deposits and withdrawals i.e. it records the history of these actions. Of course the balance has to be consistent with the transaction logs.

We need some private attributes to store the transaction logs.

class
    ACCOUNT
 
feature {NONE}
    ds:   SEQUENCE[INTEGER]
         -- History of deposits
    ws:   SEQUENCE[INTEGER]
         -- History of withdrawals
    ...
end
 

The client has readonly access to the balance and the transaction logs

feature
    balance: INTEGER
         -- The amount of money which is available on the account.
 
    deposits:    readonly SEQUENCE[INTEGER] = ds
         -- History of deposits.
 
    withdrawals: readonly SEQUENCE[INTEGER] = ws
         -- History of withdrawals.
 

Note that the client can only read the logs but is not able to modify them. In Modern Eiffel any type `T' conforms to `readonly T'.

Now we can formulate the consistency conditions that the balance must not be negative and is consistent with the transaction logs.

invariant
    balance >= 0
    balance = sum(deposits) - sum(withdrawals)
    ID(deposits) /= ID(withdrawals)
 

In the invariant we have expressed the fact that the history of the deposits is not the same object as the history of the withdrawals. This is important for the proof engine to verify the code.

In order to calculate the sum of deposits and withdrawals we use a specification function

    sum (s: SEQUENCE[INT]): INT
        note
            specification: yes   -- can only be called in assertions
            state:         no
        ensure
            Result = if s.is_empty then 0
                     else sum(s.last_removed) + s.last end
            all(s:SEQUENCE[INT]; v:INT): 
               sum(s+v) = sum(s)+v from
                  sum((s+v).last_removed) + (s+v).last = sum(s)+v
               end
        end
 

A specification function has no body, just a specification (i.e. pre- and postconditions) and can only be called in assertions.

`sum' uses an if-expression. The if-expression has an integer value. But the whole expression is a boolean expression. If-expressions within boolean expression can always be unfolded in the following manner:

    -- the boolean expression
 
    Result = if s.is_empty then 0
             else sum(s.last_removed) + s.last end
 
    -- is equivalent to
 
    s.is_empty      =>  Result = 0
    not s.is_empty  =>  Result = sum(s.last_removed) + s.last
 

Since the proof engine works with assertions (i.e. boolean expressions) it unfolds if expressions in the above way.

The class ACCOUNT contains the two commands `deposit' and `withdraw' to deposit money in the account or withdraw money from the account.

    deposit (amount: INTEGER)
        require
            amount >= 0
            no_overflow: balance <= balance + amount
        do
            ds.extend_rear(amount)
            balance := balance + amount
        ensure
            deposits = old (deposits + amount)
            balance  = old balance + amount
        end
 
    withdraw (amount: INTEGER)
        require
            amount  >= 0
            balance >= amount
        do
            ws.extend_rear(amount)
            balance := balance - amount
        ensure
            withdrawals = old (withdrawals + amount)
            balance  = old balance - amount
        end
 

Let's see how Modern Eiffel's proof engine verifies the command `deposit'. In a first step the postconditions are proved by backtransformation until they can be proved.

   -- postcondition
   balance = old balance + amount
 
   -- backtransformed through "balance := balance + amount" 
   -- by textual substitution
 
   balance + amount = old balance + amount
 
   -- backtransformed through "ds.extend_rear(amount)" which has no effect
 
   balance + amount = old balance + amount
 
   -- now we are at the start of the routine and can drop `old'
 
   balance + amount = balance + amount
 
   -- which is proved by the rule all(a:ANY): a = a
 
 
   -- postcondition
   deposits = old (deposits + amount)
 
   -- backtransformed through "balance := balance + amount" (no effect)
 
   deposits = old (deposits + amount)
 
   -- backtransformed through "ds.extend_rear(amount)" which gives
   -- (ds after) == (ds before) + amount  which implies
   -- (deposits after) = (deposits before) + amount
 
   deposits + amount = old (deposits + amount)
 
   -- now we are at the start of the routine and can drop `old' and prove
 
   deposits + amount = deposits + amount
   -- by the general rule all(a:ANY): a = a
 

Since `deposit' is an exported routine, it must preserve the invariant.

   balance >= 0
 
   -- backtransformed through "balance := balance + amount" 
   -- by textual substitution
 
   balance + amount >= 0
 
   -- ds.extend_rear(amount) has no affect, so we have at the start
 
   balance + amount >= 0 from
      0 <= balance + amount from
           -- transitivity law
           0       <=   balance             -- invariant
           balance <=   balance + amount    -- precondition
      end
   end
 

The balance has to be kept consistent with the transactions

   balance = sum(deposits) - sum(withdrawals)
 
   -- backtransformed through both commands
 
   balance + amount = sum(deposits+amount) - sum(withdrawals)
 
   -- assertion of `sum' used
 
   balance + amount = sum(deposits) + amount - sum(withdrawals) from
       balance = sum(deposits) - sum(withdrawals)   -- invariant
   end
 

All these steps are done automatically by the prove engine. No manual intervention is necessary. The SW designer just has to write the appropriate assertions.

Concurrency

Processes

An Eiffel program is a process. A process interacts with its environment by events. The most basic events for a program are its input/output events via standard input and standard output (usually the consolve). GUI programs interact with its environment by gui events like mouse clicks, button presses, output of text and graphics in windows etc.

This view is consistent with the view of nearly all currently available operating systems. If you start a program (on the console or via a desktop), the operating system creates a process in which the code of the program executes.

The environment itself can be considered a process as well. In that view we have two processes interacting, a program and its environment.

A program can start other processes and interact with them. For the external view it is still one process, but the process visible to the external world can be implemented by various interacting processes.

Tony Hoare used this basic abstraction to create his theory of Communicating Sequential Processes (CSP, see http://www.usingcsp.com/cspbook.pdf). The concurrency part of Modern Eiffel is based on CSP, i.e. an Eiffel process is a process in the sense of CSP.

The main process of an Eiffel program is started by calling its root procedure. An Eiffel program can start other processes by calling a procedure as root procedure of that newly started process.

   -- a) spawn a process by creating a separate object
 
   t: separate T
   ...
   create t.make(arg1, arg2, ...)   -- Execute the creation procedure of T
                                    -- as a concurrent process
 
   -- b) spawn a process by making a `separate' call to a procedure
 
   separate proc(arg1, arg2, ...)   -- Separate call of a procedure `proc' of
                                    -- the surrounding class. The procedure
                                    -- must be stateless! The procedure `proc' 
                                    -- is executed as a concurrent process.
 
             -- by making a `separate' call to a procecure, implicitely an
             -- object of a nameless class/type XXXX is created
             class XXX create proc feature 
                   proc  ... -- same implementation as `proc' above
             end  
 

Every process can create new objects. All objects created within a process belong to that process.

I.e. a process can interact with another process only by read/write data from/to a channel, call a procedure of a separate object (no direct query calls allowed) and execute a separate (i.e. synchronized region).

Let's assume that process `p1' makes a separate procedure call `proc' to process `p2'. Then `p1' sees the event sequence

          ... enter proc,  exit proc, ...

The semantics of Modern Eiffel guarantees that there is no event between `enter proc' and `exit proc' which is visible to process `p1'.

Since the procedure `proc' of `p2' can read from or write to channels, can do other separate procedure calls and can execute separate regions, `p2' can see the events

          ... enter proc, e1, e2, ...., exit proc, ...

The important thing: Both processes see enter and exit in the same sequence. No callback is possible from `p2' to `p1' during the execution of the procedure `proc'. The latter might be seen as a big restriction, but in reality it does not seem to restrict. On the contrary, it helps to write correct concurrent programs.

Some Eiffel processes

A process (or better its root procedure) which generates an infinite sequence of natural numbers starting from `start' and writes them to an output channel is

   separate generate_naturals(start:NAT; ch: CHANNEL[NAT])
       invariant
          all(i:INT): 0<=i and i<ch.seq.count => ch.seq[i]=start+i
       do
           from
               local i := start
           loop
               ch <- i      -- output `i' to channel `ch'
               i := i + 1
           end
       end
 

A loop without exit condition is called an event loop. The first statement in the body of an event loop must be an event. In the above case it is the output event to channel `ch'. The event loop stops if no more write events can occur on channel `ch'.

An Eiffel program which outputs the first 100 numbers generated by the process `generate_naturals' reads like

  do
      local ch: CHANNEL[NAT]
 
      generate_naturals(0, ch)             -- spawns the process
 
      across 0 .. 99 loop
          ch -> local i
          io <- i <- '\n'
      end
  end
 

Clearly this is not the most straighforward way to output the first 100 naturals on standard output. The examples just serves to demonstrate the principles.

Channels in Eiffel are unbuffered. The communication event can happen only if the writer process and the reader process are ready to write or read respectively. The write statement `ch<-i' in one process and the read statement `ch->i' on the same channel block until both processes are ready to do the communication.

A communication via a channel is a distributed assignment statement. In a sequential program one would write

     x := expr
 

Two communicating processes distribute the assignment via the statements

     -- receiving process   --------------   sending process
 
     ch -> x                                 ch <- exp
 

One advantage of processes is the possibility to combine them. The process `generate_naturals' can drive a whole chain of processes. We can write a filter which reads naturals from an input channel and outputs all number which are divisible by a certain number to its output channel.

   separate filter_remainders(
                divisor: NAT
                ch_in, ch_out: CHANNEL[NAT])
       require
           divisor > 0
       invariant
           local s := ch_in.seq.filtered(?\\divisor/=0)
           not s.is_empty => s.count-1 <= ch_out.seq.count
           ch_out.seq.is_prefix(s)
       do
           loop
             ch_in -> local i
             if i \\ divisor /= 0 
             then
                ch_out <- i
             end
           end
       end
 

The main process just combines the process to create a Unix like pipe.

  do
      local ch1, ch2: CHANNEL[NAT]
 
      generate_naturals(0, ch1)
      filter_remainders(2, ch1, ch2)
 
      across 0 .. 99 loop
          ch2 -> local i
          io <- i <- '\n'
      end
  end
 

This programm outputs the first 100 odd naturals.

Suppose that we want to calculate all prime numbers below 1000. We can use `generate_naturals(2,.)' to generate naturals starting from 2. The first number it generates is a prime number. From then on we have to let through only numbers which are not divisible by 2. We can use `filter_remainders(2,.)' to do that. This gives us the next prime number. For each new prime number we create a new filter process to let through only naturals which are not divisible by that number and soon. The main program reads

  do
      from 
          local (i:NAT := 0; ch: CHANNEL[NAT] )
          generate_naturals(2, ch)
      until
          i >= 1000
      loop
          ch -> i                          -- read
          io <- i <- '\n'                  --   and output a prime
          local ch_new := CHANNEL[NAT]     -- create a new channel
          filter_remainders(i, ch, ch_new) -- create and start the filter
                                           -- process for the current prime
          ch := ch_new                     -- from now on read from the 
                                           -- last filter
      end
  end
 

Processes and data

Up to now we have seen only processes which are represented by procedures. But a process has a root object and this root object can hold data.

In the last examples we just used the call to a stateless procedure (e.g. `filter_remainders') to create and start a process. But in reality a root object of an unnamed root type is created and the procedure is used as the creation procedure of the newly created root object.

We make this explicit by defining a class FILTER_REMAINDER and give all objects of the class two counters, one representing the number of reads and another representing the number of writes.

     separate class 
          FILTER_REMAINDER 
     create 
          make 
     feature
         count_input:  NAT    -- Number of reads
         count_output: NAT    -- Number of writes
     feature {NONE}
          make(divisor: NAT; ch_in,ch_out: CHANNEL[NAT])
             do
                 loop
                    ch_in -> local i
                    count_input := count_input + 1
                    if i \\ n /= 0 
                    then
                       ch_out <- i
                       count_output := count_output + 1
                    end
                 end
             end
     end
 

The main process has to be slightly modified to work with the new class.

  do
      from 
          local (i:       NAT := 0
                 ch:      CHANNEL[NAT]
                 filter:  detachable FILTER_REMAINDER )
          generate_naturals(2, ch)
      until
          i >= 1000
      loop
          ch -> i
          io <- i <- '\n'
          local (ch_new := CHANNEL[NAT]
                 f := FILTER_REMAINDER(i, ch, ch_new) )
                  -- create and start the filter
                  -- process for the current prime
          ch     :=  ch_new
          filter :=  f
      end
  end
 

Suppose that at the end of the main process we want to output how many nonprimes have been rejected by the last filter. The main program has a reference to the root object of the last filter. But as already said, since `filter' referes to another process the main process can only interact by communication events, separate procedure entries and exits and separate region entries and exits. Therefore the query calls `filter.count_input' and `filter.count_output' are not allowed.

In order to retrieve the counters a separate region has to be declared. This can be put at the end of the main root procedure to output the desired values.

 
    if attached filter as f then
       separate(f)
           do                 -- separate region entry event
               io <- "The last filter representing the prime "
                  <- i
                  <- " has rejected "
                  <- f.count_input - f.count_output
                  <- " numbers\n"
           end                -- separate region exit event
    end
 

The separate region entry event can happen only if the main process and the filter process participate in the events. As long as the filter process is in its event loop, it cannot accept the entry event.

Some rules

Data transfer

It is not allowed to query a separate object except in a separate region.

Reason: Outside a separate region the result of a query of a separate object is completely undefined. A separate region guarantees synchronization and allows reasoning. Outside a separate region reasoning is not possible.

If a process wants to transfer local objects to another process, the object will be cloned. This guarantees that no process has references to data of another process attached to local entities. If the object is transfered via a separate entity (declared with type `separate T' or a type which is implicitely separate) no cloning is necessary.

Data transfer between processes can occur

Modern Eiffel transfers the data either cloned or as separate entities.

Synchronization

A command of a separate object can only be called if the creation procedure of the separate object has terminated.

Only one process can call a command of a separate object (i.e. different process) at the same time. It holds a lock on the separate object during the call.

The call of a command of a separate object is only entered, if the precondition is satisfied (i.e. preconditions are wait conditions). As long as the precondition is not satisfied other processes can call other commands of the same separate object to establish the precondition.

The same applies to separate regions. In order to enter a separate region all needed separate objects must be available and the precondition must be satisfied. During execution of the separate region the current process holds a lock on all needed separate objects. This guarantees mutual exclusion.

A separate region has the general syntax

     separate(o1,o2,...)   -- o1,o2,... must be separate objects
         require
             ...           -- wait conditions
         do
             ...
         ensure
             ...           -- conditions established by the separate block
         end
 

Since command calls to separate objects and separate regions can be nested, deadlock is possible. However the runtime of a compliant Modern Eiffel compiler must be able to detect a deadlock at runtime and raise an exception or prove statically that a deadlock is not possible. Therefore a programm in written in Modern Eiffel cannot freeze.

Parallel wait (i.e. waiting faster ...)

If a process is waiting for events it can wait for more than one event. Each process can offer its environment (i.e the other processes) choices of several events. The choices can be either the guarding events of an event loop or the guarding events of an alternative command.

   loop
       case:  ch1 -> ch
              ...
       case:  ch2 <- i
              ...
       case:  sep_tgt.some_feature(a,b,c)
              ...
       case:  separate(st1,st2)
                 require
                    ...
                 do
                    ...
                 ensure
                    ...
                 end
   end
 

The above event loop offers 4 choices. It can either write to channel `ch1', or read from channel `ch2', or call `sep_tgt.some_feature(a,b,c) or enter a separate region. The first command of an alternative must be a blocking command.

The execution chooses on of the events which can happen and continues execution in that branch. If the other processes are not yet ready to engage in one of the offered events, the event loop has to wait until at least one event can happen. The event loop terminates if none of the offered events can happen any moer.

   if
       case:  ch1 -> ch
              ...
       case:  ch2 <- i
              ...
       case:  sep_tgt.some_feature(a,b,c)
              ...
       case:  separate(st1,st2)
                 require
                    ...
                 do
                    ...
                 ensure
                    ...
                 end
   end
 

In an alternative command one of the guarding events must happen eventually. Otherwise the system is deadlocked (which has to be detected by Modern Eiffel either at compile or at runtime).

Emacs postfix

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

- Introduction

- Warning: New version of Modern Eiffel available!!

- Basic motivation for Modern Eiffel and its key features

- Caveat

- Grammar

- Letter case

- Semicolons

- Annotations

- Free operators

- Feature names (overloading)

- Function declaration

- Variable declaration (scope, inferred type, etc. )

- Local routines

- Multiple assignment

- Output arguments

- Generic routines

- Types and objects

- Equality

- Hashable

- Immutability

- Type safety

- The basics

- Default inheritance

- Covariant redefinitions of arguments

- Generic constraints

- No generic conformance!

- Universal conformance

- Void safety

- Local types

- Family polymorphisms

- Kernel library

- Functions and Routines as objects (agents)

- Function objects

- General syntax

- Currying

- Scalability

- Small programs

- Scripting

- Clusters and libraries

- Class name rules

- Compiled libraries

- Verification

- Basics

- Command query separation

- Full specification

- Quantified expressions

- Construction of proof trees

- Example: class ACCOUNT

- Concurrency

- Processes

- Some Eiffel processes

- Processes and data

- Some rules

- Data transfer

- Synchronization

- Parallel wait (i.e. waiting faster ...)

- Emacs postfix


ip-location