# 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.