The Eiffel Compiler / Interpreter (tecomp)

Boolean expressions of the form

all(x:X) p(a,x) -- x is a bound variable, a is free within the expression some(x:X) p(a,x)

are not computable in general, even if the boolean valued function "p" is computable. I.e. the following constructs are illegal in executable code.

-- Illegal if expression!!! if all(x:X) p(a,x) then exp1 else exp2 end -- Illegal function definition!!! f_illegal(a:A): BOOLEAN ensure Result = all(x:X) p(a,x) end

The compiler cannot accept these constructs because it is unable to generate code to calculate the expression/function.

But a function like "f_illegal" could be very useful in assertions. Since there is no need to have runtime code for assertions, the fact that "f_illegal" is not computable does not disturb as long as it is a mathematically meaningful function.

In order to make this possible, Modern Eiffel has ghost types.

T -- a normal type ghost T -- a ghost type

Objects of ghost type are called ghost objects. Ghost objects cannot flow into real computations. But it is possible to inject ghost objects into assertions.

A function which returns ghost objects is a ghost function. Ghost functions can only be used in assertions.

With this we can define a legal version of "f_illegal".

f_legal(a:A): ghost BOOLEAN ensure Result = all(x:X) p(a,x) end

Ghost functions can be combined arbitrarly. I.e. "f_legal" is a valid definition, regardless whether "p" is a computable function or not.

Ghost functions are a powerful means to structure complicated assertions.

Functions are objects and can be passed around arbitrarily. I.e. functions can be attached to local variables, passed as arguments and returned as results.

Function objects have a type. A function receiving as argument an object of type A and returning an object of type R has the type A->R.

A->R -- function taking one argument [A,B,...]->R -- function taking many arguments []->R -- function with no argument, i.e. constant function ghost(A->R) -- a ghost function type A -> ghost R -- the same ghost function type f:A->R -- variable representing a function f[a] -- function "f" evaluated with the argument "a" g:[A,B]->R -- variable representing a function with two arguments g[a,b] -- function "g" evalutated with the arguments "a" and "b" h:[A,B]->[R,T] -- variable representing a function with two argumens -- returning two values

The function "g" is a function that maps a tuple of type [A,B] to R. But as described in the last post "Tuples and functions", sequences of expressions and tuples with matching types can be used interchangeably.

Therefore the function "g" can be called with "g[a,b]" as if it were a function with two arguments instead of "g[ [a,b] ]" which were necessary if Modern Eiffel would not have this conversion between sequences of expressions and tuple expressions.

The type A->R inherits from the type FUNCTION[A,R]. The declaration of FUNCIONT[A,R] is contained within a module "function" and looks like

-- file: function.e deferred class FUNCTION[A,R] inherit COMPARABLE end

The fact that the class FUNCTION has only two formal generics, one for the argument and one for the return type, is no restriction. A and R can be arbitrary tuples. Therefore any multiargument-multireturn function [A,B]->[R,T] can be represented as FUNCTION[ [A,B], [R,T] ].

The module "function" has the following basic functions

feature is_defined(f:CURRENT, a:A): ghost BOOLEAN -- Is the function `f' defined at argument `a'? deferred end is_total(f:CURRENT): ghost BOOLEAN -- Is the function `f' defined for all arguments? ensure Result = all(a:A) f.is_defined(a) end [] (f:CURRENT, a:A): B -- Value of function `f' at argument `a'. require f.is_defined(a) deferred end end

All functions in Modern Eiffel are potentially partial functions. The function "is_defined" represents the precondition of the function "f" and returns whether the function is defined at a certain argument.

The function "is_total" tells whether the function is defined for all possible arguments.

The function "[]" returns the value of the function at a certain argument.

Only the function "[]" can be called in computations. The functions "is_defined" and "is_total" are ghost functions and can be used only in assertions.

The operator "[]" stands for function application. The value of the function "f" at argument "a" is returned by "f[a]".

Note: We abandon the syntax of ISE Eiffel that all functions must have names and can have an optional operator alias. In the following we treat operators as first class feature names. I.e. the operator symbols "=", "<=", "/", "and", "not", "or", ... are valid feature names for functions with one argument (prefix operator) or two arguments (binary operator). The bracket operator "[]" can have an arbitrary number of arguments. This convention is essentially the same as the one used in the programming language Scala.

Mathematically functions are sets of key-value pairs. Therefore we say the two functions "f" and "g" are equal if their sets of key-value pairs are equal.

Two sets "a" and "b" are equal if "a" is a subset of "b" and "b" is a subset of "a".

The following feature block in the module "function" codes these definitions into Modern Eiffel.

feature -- equality is_contained(f,g:CURRENT): ghost BOOLEAN ensure Result = all(a:A) check f.is_defined(a) => g.is_defined(a) f.is_defined(a) => (f[a] = g[a]) end end = (f,g:CURRENT): ghost BOOLEAN ensure Result = (f.is_contained(g) and g.is_contained(a)) end is_strictly_contained(f,g:CURRENT): ghost BOOLEAN ensure Result = (f.is_contained(g) and f/=g) end end

We expect containment to be reflexive, antisymmetric and transitive and equality to be reflexive, symmetric and transitive. I.e. we expect the following assertions to be true.

feature all(f,g,h:CURRENT) check reflexive: f.is_contained(f) antisymmetric: f.is_contained(g) => g.is_contained(f) => (f=g) transitive: f.is_contained(g) => g.is_contained(h) => f.is_contained(h) reflexive: f=f symmetric: (f=g) => (g=f) transitive: (f=g) => (g=h) => (f=h) end end

The proof engine of Modern Eiffel is able to proof these properties automatically. The reader is encouraged to prove these assertions in order to see that the proofs are straighforward.

The above properties of "is_contained" and "=" satisfy the needed properties for the type "PARTIALLY_ORDERED". And indeed we can define the class FUNCTION in the following manner.

deferred class FUNCTION[A,R] inherit ghost PARTIALLY_ORDERED rename is_less_equal as is_contained is_less as is_strictly_contained end end

Note that the parent type PARTIALLY_COMPARABLE must be inherited as a ghost type because in the parent all functions are defined as computable functions. Inheriting as ghost converts all functions inherited from the parent to ghost functions.

This declaration of the class FUNCTION is highly recommendable because with PARTIALLY_ORDERED as parent the module "function" inherits all proved assertions of the parent class.

Any function can be converted to a function object. Having the function "func"

func(a:A,b:B):R require pre(a,b) ensure ... end

the following expressions are equivalent

func(a,b) -- call "func" directly local f:[A,B]->R := func -- create a function object and assign it to "f" then f[a,b] -- call the function object end

Note: While named functions like "func" are called in the usual manner with parenthesized arguments, anonymous functions (i.e. function objects) are called with the arguments provided in brackets.

The possibility gets interesting if we start to pass around function objects.

-- assume `gfunc' has the definition gfunc(f:[A,B]->R, x:X): T require ensure ... end -- then the following expression is valid gfunc(func,x)

Any expression can be used to create a function object. Suppose we have an expression "e" then "x->e" is a function which maps any argument to the value of "e" with "x" replaced by the argument, i.e. "(x->e)[y]=e[x:=y]".

-- general rule x->e (x->e)[y] = e[x:=y] -- some examples i->i+1 (i->i+1)[5] = 6 (i->i+1)[n+m] = (n+m)+1 i->(i+j)/k (i->(i+j)/k)[10] = (10+j)/k

In the expression "x->e" the variable "x" is a bound variable. It can be renamed arbitrarly (but consistently on the left and the right hand side of the arrow).

(x->e) = (y->e[x:=y]) (x->e) = (z->e[x:=z])

Some more possibilities to create function objects from expressions.

x:X->e -- explicitly typed argument [x,y,..]->e -- multiargument function [x:X,y:Y,...]->e -- multiargument function with explicitly typed arguments -- call of the function [x,y]->e ([x,y]->e)[a,b] = e[x,y:=a,b]

All functions are potentially partial, i.e. they can have preconditions. The preconditions are handed over to the function "is_defined" of the function object.

In the above example the function "func(a:A,b:B):R" has the precondition "pre(a,b)". Therefore in the corresponding function object "f" the expression "f.is_defined(a,b)" has the same value as "pre(a,b)".

The same applies to function objects created from expressions. Any expression "e" can have a set of preconditions "p1", "p2", ...

e -- an expression p1,p2,... -- the precondition expressions of e (x->e).is_defined(y) = check (x->p1)[y], (x->p2)[y], ... end

Example

a/b -- e.g. division of natural numbers b/=0 -- precondition of "a/b" b->a/b -- function where the divisor is taken as the argument (b->a/b).is_defined(i) = (i/=0)

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