The Eiffel Compiler / Interpreter (tecomp)
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.
Modern Eiffel combines elements of object oriented programming and functional programming in one language.
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
where the target "t" represents an object of a type created from the class C. In functional programming this call would we written as
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++, ...).
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.
In Modern Eiffel the first argument of a call can be given in dot notation. The two expressions
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
are usally preferred to the expressions
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
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.
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.
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.
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.
Local Variables: mode: outline coding: iso-latin-1 outline-regexp: "=\\(=\\)*" End: