The Eiffel Compiler / Interpreter (tecomp)
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 the object.
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.
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 for 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.
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.
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 specified.
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 computations.
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 hierarchy.
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 "some_procedure".
The verifier augments the above specification to the following complete specification
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 following 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 code snippet
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.
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
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
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 classes.
Local Variables: mode: outline coding: iso-latin-1 outline-regexp: "=\\(=\\)*" End: