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.
