In the course of this blog I am going to use a variant of Eiffel called
“Modern Eiffel”. This blog entry gives a short outline of the language
elements. Although “Modern Eiffel” is a full blown language with all
sorts of imperative elements, mutable reference type objects, multiple
inheritance, dynamic bind etc. this blog entry concentrates only on a
small subset: immutable types and inductive types. The reason:
immutable/inductive types are a very important concept to verify
statically the correctness of a program. More advanced features will be
introduced if necessary.
Skeleton of a class
Modern Eiffel is an object oriented language. All types are defined by
classes (as in other object oriented languages like C++, C#, java,
scala, etc.). The skeleton of a class looks like
class MY_CLASS -- class name create creator1(a:A) ... creator2 ... feature some_function(b:B): RT ... some_command(c:C) ... all(i:INT) some_property(i) proof ... end CHAR = CHARACTER -- type alias invariant ... -- consistency conditions end
Comments begin with “–” and span to the end of the line.
Classes and types are always written in uppercase. Each class can have
creators by which objects of the corresponding type can be constructed.
The features of a class are either functions (i.e. routines which return
a value) or commands (i.e. routines which change the state of the
object) or assertions or type aliases.
There are some basic types. These are types with built-in functions and
built-in value representation. The basic types are BOOLEAN, NAT
(unsigned integers of a certain size), INT (signed integers of a certain
size). Beside their built-in functions and value representation the
basic types are nothing special. They are defined with classes as well.
immutable class BOOLEAN feature implication alias "=>" (o:BOOLEAN): BOOLEAN external "built_in" end negated alias "not": BOOLEAN external "built_in" end conjuncted alias "and" (o:BOOLEAN): BOOLEAN external "built_in" end disjuncted alias "or" (o:BOOLEAN): BOOLEAN external "built_in" end ... end
Functions can have operator aliases for unary and binary operators. I.e.
having variables a,b,c of type BOOLEAN the expressions
not a -- highest precedence a and b a or b a => b -- lowest precedence
have the expected meaning. The most important boolean operator is the
implication “=>”. It is right associative i.e. “a => b => c” is parsed
as “a => (b => c)”. The binary operators “and” and “or” are left
associative. All binary boolean operators are not strict (short
circuited) i.e. the second operand is only evaluated if necessary to
determine the truth value of the expression.
Default inheritance and equality
A class can inherit features from other classes. For this blog entry
inheritance plays a minor role. I just mention the fact that each class
has some implicit inheritance. A class T with no inheritance clause is
treated as if it were defined as
class T inherit COMPARABLE ... end
The parent class COMPARABLE defines equality. It has the outline
class COMPARABLE feature is_equal(o:like Current): BOOLEAN external "built_in" ensure all(x:like Current) x=x all(x,y: like Current) x=y => y=x all(x,y,z: like Current) x=y => y=z => x=z -- "=" has higher precedence than "=>" end end
The feature “is_equal” is used in Modern Eiffel to define equality. It
is a built-in function which guarantees properties which are expected
from an equivalence relation. Reflexivity (every entity is equal to
itself), symmetry and transitivity. In Modern Eiffel the postconditions
of built-in routines are treated as axioms, i.e. properties which do not
need any proof. Note the transitivity law written as
x=y => y=z => x=z
Usually one would expect the transitivity law written as
x=y and y=z => x=z
Both forms are equivalent. This will be proved later. If possible we
write all properties with the implication operator, because implication
is more powerful and practical for proofs.
Each class inheriting from COMPARABLE can redefine (i.e. overwrite) the
feature “is_equal”. The postconditions are inherited but in case of
redefinition they are no longer treated as axioms; they have to be
proved to be true.
Simple inductive types
People with experience in imperative languages like C++, C#, Java, etc.
are not acustomed to use inductive types. People having experience with
functional languages like Haskell, ML, OCAML, COQ, Isabelle know
inductive types well. This chapter is written for people not knowing
inductive types. The others might just be interested to learn how
inductive types are presented in Eiffel syntax.
Inductive data types are best explained with some examples. The simplest
inductive type is similar to an enumeration type in other languages. We
can define a class COLOR like
case class COLOR create red green blue end
The keyword “case” introduces an inductive class. The class COLOR has
just three creators to define objects of type color. E.g. we can use
this class to define variable of type COLOR.
r: COLOR := red g: COLOR := green ...
The assigment operator “:=” can be used to initialize variables.
In a similar fashion we can define a class WEEKDAY
case class WEEKDAY create monday thuesday wednesday ... sunday feature next: WEEKDAY ... end
The class WEEKDAY has a feature “next” in order to calculate the next
weekday. The definition of “next” looks like
next: WEEKDAY = inspect Current case monday then thuesday case thuesday then wednesday ... case sunday then monday end
Inductive types allow case expression to make distinctions on how the
object has been constructed. The keyword “Current” returns the current
object. For each creator a cause clause is given. The meaning should be
quite clear. It is like C’s select statement.
The above form is the short form of a function definition. The function
“next” does not have any precondition. Therefore the short form is
appropriate. In the case that a function has preconditions, the long
form must be used.
next: WEEKDAY require ... -- precondition(s) ensure Result = inspect Current case monday then thuesday ... end end
The keyword “Result” indicates the return value of the function. The
postcondition “Result = … ” specifies the return value of the function.
Inductive types with stored values
Objects of the very simple inductive types like COLOR and WEEKDAY just
store as its value the way they have been constructed. But objects of
inductive type can store other values as well.
Let us consider the following class
case class OPTIONAL[G] create none value(value: G) end
This class is generic. A generic class is a type constructor. It can
construct the types OPTIONAL[INT], OPTIONAL[BOOLEAN], OPTIONAL[COLOR],
The class has just two creators: “none” and “value”. The object
n: OPTIONAL[INT] := none
has no value and the object
i7: OPTIONAL[INT] := value(7)
has the value 7. The name “value” is used for the creator and for an
attribute. The attribute “value” is an optional attribute. It is
available only if the object has been created with the “value” creator.
The access of the attribute “value” is illegal, if the corresponding
object has not been created with the “value” creator. In many case the
attribute is not accessed directly. Usually the attribute is accessed
better through pattern matching expressions.
In order to introduce pattern matching we use a contrived example of a
value_plus_100(o:OPTIONAL[INT]) = inspect o case none then -1 case value(i) then i+100 end
The function “value_plus_100 is contrived, because one would not write
such a function in Modern Eiffel. The inspect expression distinguishes
the two possible creators for an object of type OPTIONAL[INT].
The first case clause is for objects created with the “none” creator.
Since the “none” creator has no arguments, no value can be extracted in
The second case clause is for objects which have been created with the
“value” creator. This creator has one argument which can be retrieved
and attached to a fresh local variable with name “i”. This variable is
availalbe only on the right hand side of this case clause to calculate
the return value.
The function “value_plus_100″ can be written in a form which accesses
the attribute “value” directly.
value_plus_100(o:OPTIONAL[INT]) = inspect o case none then -1 case value(_) then o.value + 100 end
The wild card “_” is used to supress the creations of a fresh local
variable. But the compiler derives the fact that in this case clause the
object “o” has been created with the “value” creator. Therefore the
access to the attribute “value” is valid within this clause.
Inductive types with recursive structure
The full expressive power of inductive types unfolds with recursively
defined inductive types. We can use an inductive type to define natural
case class UNARY_NATURAL create zero succ(pred: UNARY_NATURAL) feature plus alias "+" (o:UNARY_NATURAL): UNARY_NATURAL = ... times alias "*" (o:UNARY_NATURAL): UNARY_NATURAL = ... power alias "^" (o:UNARY_NATURAL): UNARY_NATURAL = ... ... end
The class UNARY_NATURAL is highly inefficient to do arithmetics. But it
is a good vehicle to model natural numbers and use this model to prove
properties of very efficient implementations of natural numbers.
The class UNARY_NATURAL has tow creators. One to create the number 0 and
one to create the successor of an already created number.
The recursive structure of the type can be used to define the functions
“plus”, “times” and “power” recursively.
plus alias "+" (o:UNARY_NATURAL): UNARY_NATURAL = inspect Current case zero then o case succ(p) then succ(p+o) end times alias "*" (o:UNARY_NATURAL): UNARY_NATURAL = inspect Current case zero then zero case succ(p) then o + p*o end power alias "^" (o:UNARY_NATURAL): UNARY_NATURAL = inspect o case zero then succ(zero) case succ(p) then Current * Current^p end
Recursive functions for inductive types defined in this fashion have the
nice property that the compiler can verify the termination of the
recursion. In order to see this let us look at the recursive branch of
the definition of “+”
case succ(p) then succ(p+o)
This branch is entered only if the current object has been created with
the “succ” creator using an already existing number, the predecessor of
the current object. The left hand side of the case expression attaches
the predecessor of the current object to the fresh local variable “p”.
The right hand side
uses the predecessor to make the recursive call “p+o”, i.e. it calls the
function “plus” recursively. This recursive call will finally terminate
i.e. end up in a branch “case zero”, because the very first creator of
any UNARY_NATURAL number must have been the “zero” creator. This is the
only way to create a UNARY_NATURAL if no other UNARY_NATURAL is available.
Another classic inductive type is defined by the class LIST.
case class LIST[G] create nil cons alias "::" (first:G; tail:LIST[G]) feature ... end
A list is either empty or is an element (the first element) followed by
another list (the tail of the newly created list).
If a creator has two arguments, a binary operator can be used as an
alias. All binary operators ending with “::” are right associative.
Therefore the following initialization of variables is well defined
lst: LIST[INT] := 1::2::3::nil -- parsed as 1::(2::(3::nil)) -- equivalent to cons(1,cons(2,(cons(3,nil)))
Since lists are very expressive on its own and can serve as models an
extra blog entry will be dedicated to lists.
This blog has introduced some basic language elements of Modern Eiffel.
Some next blog entries will concetrate more on lists and on how to prove
assertions within Modern Eiffel.
Keep in mind that all sorts of mutable structures and imperative
elements are possible in Modern Eiffel. But in order to verify SW
immutable types and especially inductive types are very important.
Therefore this blog will first scrutinize immutable types.