Modern Eiffel has immutable and mutable types. An object of immutable type
cannot be modified, an object of mutable type can be modified. Therefore we
say that an object is mutable or immutable depending on its type.
Immutable objects don’t have an own identity. The identity of an immutable
object is completely determined by its value. Immutable objects are therefore
sometimes called value objects and the corresponding types are called value
types. All mathematical objects like numbers, lists, sets are immutable. We
can assign to a variable a different immutable object, but we cannot modify
I.e. immutable objects are like numbers. The number “5″ is the number “5″ and
remains forever the number “5″. We can assign the number “5″ to a variable by
“i:=5″. The we can double the content of the variable “i” by the statement
“i:=2*i”. Now the value of the variable is the number “10″. But the assignment
did not change the number “5″.
Real life objects have identity. Your car is your car and your neighbours car
is a different car. The car factory puts a serial number into the chasis to
identify the car. The motor of your car has an identity with its own serial
number. You can put another motor in your car. This does not change the
identity of your car. Your car just got a new motor which is different from
the previous motor. I.e. cars are mutable, you can modify them.
A programming language which wants to be able to model real life objects must
have have mutable objects with identity. Therefore in Modern Eiffel we make
the distinction between immutable and mutable types.
Equality and identity
Since immutable type objects do not have an own identity all immutable type
objects must have an equality relation “=”. The language rules enforce that
“=” must be defined in a way that equality implies identity. I.e. if two
expressions “e1″ and “e2″ return equal objects we can always substitute the
subexpression “e1″ by “e2″ and vice versa in all expressions. This property
is called “referential transparency” sometimes expressed as “substitute equals
This is not true for mutable type objects. For mutable type objects “equality”
does not guarantee “identity”. Two expressions “e1″ and “e2″ of mutable
type might return equal objects. But this is not sufficient to conclude that
both objects are identical. I.e. we cannot substitute the subexpression “e1″
by “e2″ within an expression by knowing only that both objects are equal. The
substitution is allowed only if the expression “e1″ and “e2″ guarantee that
they return the same object.
In order to distinguish equality and identity we have two operators.
= -- Equality: reflexive, symmetric and transitive relation ~ -- Identity: reflexive, symmetric and transitive relation
The language rules guarantee the following properties:
all[G](a,b,c:G) note built_in ensure reflexive: a~a symmetric: (a~b) => (b~a) transitive: (a~b) => (b~c) => (a~c) functions: all[H](f:G->H) f.is_defined(a) => (a~b) => (f[a]~f[b]) end all[G:COMPARABLE](a,b:G) note built_in ensure identity: (a~b) => (a=b) end all[immutable G](a,b:G) note built_in ensure no_identity: (a=b) => (a~b) end
In order to enforce these properties Modern Eiffel imposes the following
restrictions on the definition of types.
- For immutable types equality must be defined in a way that “no_identity” is
guaranteed. I.e. equality must use all visible attributes of a type to
defined equality. For inductive types the compiler generates the equality
function in a consistent manner.
- The equality operator “=” can be assigned to a functions only if the
function is inherited from the class COMPARABLE. The operator “=” is
reserved for this function.
- The class COMPARABLE can be inherited multiply, i.e. it is possible to
define various equivalence relations for a type. In order to achieve this
the operator “=” can be renamed (e.g. =.alpha, =.beta, …). But immutable
types must always have one inheritance of COMPARABLE without rename of “=”
which guarantees the property “no_identity”.
Example of a mutable type: BUFFER
User’s view only
In the following we give just the specifications of functions and procedures
i.e. we describe only the view of a potential user of the module.
A complete definition of a routine looks like
some_routine(a:A) require pre_1; pre_2; ... do cmd_1; cmd_2; ... ensure post_1; post_2; ... end
The specification part only contains
some_routine(a:A) require pre_1; pre_2; ... ensure post_1; post_2; ... end
This specification says that “some_routine” is an effective routine (it is not
deferred) and that the implementation is given at a different location.
The basic access functions
For the user a buffer is a generic class.
class BUFFER[G] -- A bounded buffer of elements of type G implemented -- as contiguous memory cells end
A buffer has a certain maximum capacity and a content.
feature capacity(b:CURRENT): NATURAL -- The capacity of the buffer. content(b:CURRENT): ghost LIST[G] -- The content of the buffer. end
The content is a ghost function, i.e. it can be used only in
assertions. Having these two basic functions a lot of useful functions can be
feature count(b:CURRENT): NATURAL -- The number of elements in the buffer. ensure Result = b.content.count end  (b:CURRENT, i:NATURAL): G -- The i-th element of the buffer. require i < b.count ensure Result ~ b.content[i] end is_empty(b:CURRENT): BOOLEAN ensure Result = (b.count = 0) end is_full(b:CURRENT): BOOLEAN ensure Result = (b.count = b.capacity) end first(b:CURRENT): G require not b.is_empty ensure Result ~ b.content.first end last(b:CURRENT): G require not b.is_empty ensure Result ~ b.content.last end end
Recall that we just give the specification here. The function “count” is
specified based on the function “content”. This says nothing about the
implementation. Certainly the implementation has to do it differently because
“content” is a ghost function and therefore cannot be used in actual
The complete set of functions has the following dependency graph (from the
users point of view).
Dependency graph is_empty is_full | / | | / | first last  count..../ | \ \ \ / | \ \ \ / | \ \ \ / | .......... content capacity
The dependency graph must reflect a hierarchy, i.e. a partial order. Cyclic
definitions are not allowed. Therefore there are always functions which do not
have a specification i.e. functions which are at the bottom of the dependency
The dependency graph is used by the user to derive the effect of modifying
procedures. The basic rule in Modern Eiffel: A procedure must not have any
unspecified effects. Let’s assume the following procedure specification
some_procedure(b:CURRENT) ensure not b.is_empty end
This procedure may change a lot but not everything. It affects “is_empty”,
therefore it must have affected “count” and “content”. A modification of
“content” might affect “first”, “last” and “” as well. The only function
which must not be affected by “some_procedure” is “capacity”. This is the
implicit framing condition which the user can derive from the specification or
The verifier augments the above specification to the following complete
some_procedure(b:CURRENT) ensure not b.is_empty all(a:CURRENT) a.capacity = old a.capacity all(a:CURRENT) require a /~ b ensure a.is_empty = old a.is_empty a.count = old a.count a.content = old a.content -- needs to be kept end end
The algorithm to derive the implicit contract is straightforward. The
postcondition states that “is_empty” might have changed. This has the
- All basic functions at the bottom of the dependency graph on which
“is_empty” does not depend are unchanged.
- The function “is_empty” is only changed for the given argument “b”. For
other arguments it is unchanged.
- The fact that “is_empty” is unchanged for arguments different from “b” is
propagated down the dependency graph (only the conditions for the basic
functions need to be kept, the others are consequences).
It would be very tedious to write these complete specifications. Therefore the
compiler has to derive them automatically. I.e. the user of “buffer” has these
conditions available to prove its own routine and the proof engine verifies
that the implementation of “buffer” respects the implicit frame contract.
Mutable objects can be created and modified. It is possible to require some
consistency conditions which are always satisfied by any object of a certain
type. These consistency conditions are called invariants.
Each creation procedure has to establish the invariant and each procedure
which modifies the object has to maintain the invariant.
The buffer is supposed to guarantee the invariant that it does not contain
more elements than is allowed by its capacity.
invariant all(b:CURRENT) b.count <= b.capacity end
Note that an invariant is something different from other assertions. E.g. the
module buffer guarantees the assertion
feature all(b:CURRENT) b.count = b.content.count end
But this is not an invariant. This condition is already guaranteed by the
specification of the function “count” (see declaration above) which any
implementation of “count” has to respect. I.e. this assertion is not a
requirement for creation procedures and other procedures.
A buffer can be created with the creation procedure “with_capacity”. I.e. the
local b: BUFFER[STRING] do create b.with_capacity(100) ... end
creates an empty buffer with the capacity to store 100 strings. The creation
procedure is specified as
create with_capacity(b:CURRENT, c:NATURAL) ensure b.content = nil b.capacity = c end end
The verifier has to check that “with_capacity” establishes the invariant. The
proof of the invariant “b.count<=b.capacity” is trivial given the
postcondition of “with_capacity”. Since “b.content=nil” and “nil.count=0″ we
have “b.count=0″ which satisfies the invariant.
The compiler derives from the specification of the creation procedure
“with_capacity” the complete contract including framing conditions
create with_capacity(b:CURRENT, c:NATURAL) ensure b.content = nil b.capacity = c all(a:CURRENT) require a /~ b ensure a.content = old a.content a.capacity = old a.capacity end end
Since the object is created by “create b.with_capacity(100)” the compiler
derives the obvious fact that the newly created object is not identical with
any existing object (otherwise it were not new). This fact together with the
complete contract allows the user to verify the code following the creation of
an object. The verifier can derive that no existing object will be changed
after the creation of a new one.
Insert and modify elements
We can insert elements at the rear end and at the front end, we can overwrite
an element at a certain position and we can rotate the whole buffer.
The following code specifies these procedures.
feature extend_rear(b:CURRENT, e:G) -- Append element `e' at the end of buffer `b' require not b.is_full ensure b.content = old (b.content + e) end extend_front(b:CURRENT, e:G) -- Prepend element `e' at the front of buffer `b' require not b.is_full ensure b.content = old (e :: b.content) end put(b:CURRENT, i:NATURAL, e:G) -- Overwrite element at position `i' with `e' within the buffer `b'. require i < b.count ensure b.content = old (b.content.take(i) + e + b.content.drop(i+1)) end rotate_up(b:CURRENT) -- Rotate the content of the buffer up. require not b.is_empty ensure b.content = old (b.content.last + b.content.without_last) end end
The compiler derives for all these procedures a complete contract. E.g. for
the procedure “extend_rear” it derives the complete frame contract.
extend_rear(b:CURRENT, e:G) -- Append element `e' at the end of buffer `b' require not b.is_full ensure -- complete frame contract b.content = old (b.content + e) all(a:CURRENT) a.capacity = old a.capacity all(a:CURRENT) require a /~ b ensure a.content = old a.content end end
The complete frame contract is a requirement for the implementation. The user
of “extend_rear” can rely on the complete frame contract. Since the complete
frame contract is derived automatically there is no need to type it in. The
basic contract “b.content = old b.content + e” is sufficient.
Even if the implementation is not yet available it is possible to proof that
the invariant is maintained (i.e. the invariant is valid at the end if it has
been valid at the entry point. The proof can be done by the proof engine so
there is no need to provide a proof. We give an explicit pedantic proof here
in order to demonstrate that the proof is a triviality.
all(b:CURRENT, e:G) require not is_full b.count <= b.capacity do check b.count /= b.capacity -- "not is_full" b.count < b.capacity b.content.count < b.capacity b.content.count + 1 <= b.capacity (b.content+e).count <= b.capacity end extend_rear(e) check b.content.count <= b.capacity end ensure b.count <= b.capacity end
Multiple equivalence relations with multiple inheritance
For the type BUFFER there are two equivalence relations which make
sense. Either consider two buffers equal if they have the same content or
consider them equal if they have the same content and the same size.
In Modern Eiffel we have multiple inheritance with replication. This allows us
to have both relations in the same type.
Remember that the abstract class COMPARABLE defines an equivalence
relation. The module “comparable” looks like
deferred class COMPARABLE end feature = (a,b:CURRENT): BOOLEAN deferred end all(a,b,c:CURRENT) deferred ensure a=a (a=b) => (b=a) (a=b) => (b=c) => (a=c) end end
This module has a deferred predicate “=” and some deferred proofs. An
effective module which implements COMPARABLE has to implement “=” and provide
the proofs for reflexivity, symmetry and transitivity.
In the class BUFFER we just inherit COMPARABLE twice.
class BUFFER[G] inherit COMPARABLE COMPARABLE rename = as =.content end end feature =.content (a,b:CURRENT): BOOLEAN ensure Result = (a.content = b.content) end = (a,b: CURRENT): BOOLEAN ensure Result = (a.content=b.content and a.capacity=b.capacity) end end
The proofs of reflexivity, symmetry and transitivity are trivial and derived
automatically. Clearly the predicates “=” and “=.content” need an
implementation because their specification is based on ghost functions
i.e. not executable.
Having these two equivalence relations we can use expressions of the form
local a,b: BUFFER[NATURAL] do ... if a = b then ... end if a =.content b then ... end end
For those who prefer unqualified calls
In the above code all procedures and functions have been taken out of the
class in order to make the arguments more explicit. This is not necessary. As
long as the first argument of a function or a procedure is of the current
type, we can put these routines back into the class. I.e. it is possible (and
maybe more convenient) to write specifications like
class BUFFER[G] feature count: NATURAL -- The number of elements in the buffer. ensure Result = content.count end  (i:NATURAL): G -- The i-th element of the buffer. require i < count ensure Result ~ content[i] end ... invariant count <= capacity end class BUFFER[G] feature extend_rear(e:G) -- Append element `e' at the end of the buffer require not is_full ensure content = old (content + e) end end
Note that the file “buffer.e” can have more than one class block with the same
class. The class declarations are handled cumulatively. The first class block
might just declare the class “class X end”. A second block might specify the
inheritance relation “class X inherit P end. Other blocks can specify
features, invariants, assertions, etc.
Standalone feature blocks can be used to specify static features
(i.e. routines which do not have an implicit first argument of type CURRENT).
One block might just specify a routine, another block (in the corresponding
implementation file) can implement the routine.
This gives a lot of flexibility in declaring, specifying and implementing