SourceForge.net LogoThe Eiffel Compiler / Interpreter (tecomp)

doc/papers/proof/module

Specification and implementation of modules

Definition of a module

A module is a compilation unit. It is contained in a file e.g. "c.e". A module file contains a sequence of blocks. Each block is either a class block or a feature block, i.e. a module file has the structure

  -- file "c.e"
  class  C ... end
 
  feature ... end
 
  feature ... end
 
  class X ... end
 
  ...
 

A class with the same name as the module is called the module's current class. In many cases a module contains just its current class and no other classes.

Note that the current class C can be simple or generic. If it is simple it creates the type C. If it is generic (e.g. class C[G1,G2,...]) it can create types where the formal generics G1,G2,... are replaced by actual generics A1,A2, ... If the current class is generic the module is generic as well.

If the module has a current class then it has an implicitly defined type CURRENT which is equivalent to C[G1,G2,...] in the current module. The type CURRENT is called the current type of the module.

Functional and object oriented programming style

Modern Eiffel combines elements of object oriented programming and functional programming in one language.

Differences between object oriented and functional style

Usualy in object oriented languages we define functions and procedures within classes in the form

  class C feature
    ...
    f(a:A; b:B; ... ): RT
         -- A function `f' with arguments a,b,... of type A,B,... returning
         -- a result of type RT
    ...
  end
 

and call it with the syntax

  t.f(a,b,...)
 

where the target "t" represents an object of a type created from the class C. In functional programming this call would we written as

  f(t,a,b,...)
 

Object oriented programming has the convention that each function has an implicit first argument (called "this", "self", "Current", ...). This implicit argument is provided in an actual call with a dot notation. Therefore all defined functions and procedures have one argument more than explicitely written in the definition.

It is also possible to define routines which do not have this implicit first argument by marking the definition of the routine with a special keyword (e.g. static in java, C++, ...).

Conventions in Modern Eiffel

In Modern Eiffel we can define the routines outside of the classes in feature blocks. E.g. we can write a module "unary_natural" which looks like

  -- file "unary_natural.e"
  case class
    UNARY_NATURAL
  create
    zero
    succ(pred:UNARY_NATURAL)
  end
 
 
  feature
    plus alias "+" (a,b: UNARY_NATURAL): UNARY_NATURAL
      ensure
        Result = inspect b
                 case zero    then a
                 case succ(p) then succ(a+p)
                 end
      end
 
    times alias "*" (a,b: UNARY_NATURAL): UNARY_NATURAL
      ensure
        Result = inspect b
                 case zero     then zero
                 case succ(p)  then a*p + a
                 end
      end
 
    ...
  end
 

This notation has the advantage that we can define functions where the first argument is not necessarly of main type of the module. With this notation there is no need to define "static" functions. All arguments are written explicitely. If the first argument is not of the current type then the routine is equivalent to a static routine in other programming languages.

Calls in Modern Eiffel

In Modern Eiffel the first argument of a call can be given in dot notation. The two expressions

  a.plus(b)
  plus(a,b)
 

are semantically equivalent. Usually the first one is preferable because of readability. Consider e.g. a module "set" with the definitions

  class SET[G] ... end
 
  feature  
    is_empty(s:CURRENT): BOOLEAN ... 
    is_in alias "in" (e:G; s:CURRENT): BOOLEAN ...
    ...
  end
 

The expressions

  s.is_empty
  e.is_in(s)
 

are usally preferred to the expressions

  is_empty(s)
  is_in(e,s)
 

The dot notation is the recommended style.

Since the function "is_in" has an operator alias we can even write

  e in s
 

which is more readable and intuitive than

  e.is_in(s)
 

Attributes are functions

Consider a class POINT with two attributes

  class
    POINT
  feature
    x: FLOAT
    y: FLOAT
  end
 

If we have an object "p", we can retrieve the coordinates by "p.x" and "p.y". The expressions "p.x" and "p.y" are function calls from a user perspective. I.e. from a user point of view the above module looks as if it has the definition

  class
    POINT
  end
 
  feature
    x(p:POINT): FLOAT
    y(p:POINT): FLOAT
  end
 
  ...
 

I.e. "x" and "y" are functions which map points to its coordinates.

The fact that "x" and "y" are attributes is an implementation decision which is not interesting to the user. If we decide to use polar coordinates in the implementation of POINT, then the part of the source code which declares "x" and "y" as functions i.e. the specification part does not need to change. The next chapter shows how to separate specification and implementation.

Separate specification and implementation of modules

Abstraction is very important to manage complexity. A specification of a module is an abstraction. Modern Eiffel allows to separate the specification and implemenation of modules.

If we want to write a module "m" we can create either one file "m.e" where all sources related to "m" (implementation of functions and procedures, proofs, ...) are contained or we can write two files "m.e.spec" and "m.e.imp" where the file "m.e.spec" contains just the specifications.

Example POINT

Consider the above mentioned class POINT. We can write a specification file

  -- file: "point.e.spec"
  class POINT end
 
  feature 
    x(p:POINT):FLOAT
    y(p:POINT):FLOAT
  end
 
  ...
 

and an implementation file

  -- file "point.e.imp"
  class
    POINT
  feature
    x: FLOAT
    y: FLOAT
  end
 
  ...
 

The class POINT has a declaration in the file "point.e.spec" which just states that it is a simple class. Nothing is said about attributes in the specification file.

The file "point.e.imp" refines the declaration of POINT. It states that the class POINT is implemented with two attributes.

Example: UNARY_NATURAL

The class UNARY_NATURAL used in the article "Reasoning with inductive types" can be split in a specification and a declaration file as well.

The specification file can look like.

  -- file: "unary_natural.e.spec"
  case class
    UNARY_NATURAL
  create
    zero
    succ(pred:UNARY_NATURAL)
  end
 
  feature  -- plus
    plus alias "+"  (a,b:UNARY_NATURAL): UNARY_NATURAL
      ensure
        Result = inspect b 
                 case zero    then a 
                 case succ(p) then succ(a+p) end
      end
 
    all(a,b,c:UNARY_NATURAL) check
      a + zero = a
      zero + a = a
      a + b = b + a
      a + b + c = a + (b+c)
    end
  end
 

The class "unary_natural.e.spec" contains all information needed for users of the module. All the proofs of the assertions are not needed by the user. Therefore the proofs can be put into the implementation file.

An implementation file for unary naturals can look like:

  -- file: "unary_natural.e.imp"
  feature
    all(a,b,c:UNARY_NATURAL) check
       a + zero = a
         proof ... end
 
      lemma: a as succ(_) => a+b = succ(a.pred+b)
         proof ... end
 
       zero + a = a
         proof ... end
 
       a + b = b + a
         proof ... end
 
      lemma_1: b as succ(_) => (a+b) as succ(_)
         proof ... end
 
      lemma_2: b as succ(_) => a+b.pred = (a+b).pred
         proof ... end
 
 
       a + b + c = a + (b+c)
         proof ... end
    end
  end
 

Note that the implementation file can define some lemmas which are needed to proof the main assertions. The assertions of the specification file are restated and augmented with proofs.

Emacs suffix

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

- Definition of a module

- Functional and object oriented programming style

- Differences between object oriented and functional style

- Conventions in Modern Eiffel

- Calls in Modern Eiffel

- Attributes are functions

- Separate specification and implementation of modules

- Example POINT

- Example: UNARY_NATURAL

- Emacs suffix


ip-location