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
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 as objects
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 module “function”
The class FUNCTION
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] ].
Basic functions of the module “function”
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
The function “value” returns the value of the function at a certain argument.
Only the function “value” can be called in computations. The functions
“is_defined” and “is_total” are ghost functions and can be used only in
The operator “” stands for function application. The value of the function
“f” at argument “a” is returned by “f[a]”.
Note: We leave 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.
Equality of functions
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
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
Properties of containment and equality
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.
Parent class of FUNCTION
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.
Creation of function objects
Convert functions into function objects
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)
Create function objects from expressions
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) = 6 (i->i+1)[n+m] = (n+m)+1 i->(i+j)/k (i->(i+j)/k) = (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
(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]
Preconditions of function objects
All functions are potentially partial, i.e. they can have preconditions. The
preconditions are handed over to the function “is_defined” of the function
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
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)