SourceForge.net LogoThe Eiffel Compiler / Interpreter (tecomp)

doc/papers/proof/lang outline

Outline of Modern Eiffel

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.

Basic types

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 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 is not important. 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
      -> ANY
      COMPARABLE
   ...
   end
 

The symbol "->" stands for conforming inheritance. For the following the class ANY is not important. But 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 that 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.

Inductive types

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 variables 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 function "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 expressions 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], OPTIONAL[OPTIONAL[CHARACTER]], ...

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 cases 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 function.

  value_plus_100(o:OPTIONAL[INT]): 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 that case.

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 available 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 creation 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 numbers.

  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 inefficient to do arithmetics. But it is a good vehicle to model natural numbers and this model can be used to prove properties of efficient implementations of natural numbers.

The class UNARY_NATURAL has two creators. One to create the number "zero" 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 p*o + o
    end
 
  power alias "^" (o:UNARY_NATURAL): UNARY_NATURAL =
    inspect o
    case zero    then succ(zero)
    case succ(p) then Current^p * Current
    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

   succ(p+o)
 

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.

Summary

This blog has introduced some basic language elements of Modern Eiffel. Some next blog entries will concentrate 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 the following entries will scrutinize immutable types before mutable types are introduced.

Emacs suffix

 Local Variables: 
 mode: outline
 coding: iso-latin-1
 outline-regexp: "=\\(=\\)*"
 End:
Table of contents

- Skeleton of a class

- Basic types

- Default inheritance and equality

- Inductive types

- Simple inductive types

- Inductive types with stored values

- Inductive types with recursive structure

- Summary

- Emacs suffix


ip-location