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.

Advertisements
  1. Leave a comment

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

%d bloggers like this: