Predicates, ghost predicates and higher order predicates


Predicates play an important role in specifying functions and
procedures. Since predicates are mainly used within assertions (i.e. within
contracts) it is often not necessary that predicates are computable. We often
use predicates to express not computable properties and give them a concise
name instead of repeating a long and clumsy boolean expression over and over

Predicates can be identified with sets. A set associated with a predicate is
the set of all objects which satisfy the predicate.

Basic definitions

A predicate over a type T is a boolean valued function T->BOOLEAN. But the
fact that all functions are potentially partial is disturbing for
predicates. We want that predicates are total, i.e. they can be applied to all
arguments without any restriction.

In order to distinguish between predicates and functions we use the notation

  p: T?

to express that “p” is a predicate over the type T. E.g. we can define a
predicate which says that a specific natural number is at least “5”.

  is_five_or_more(n:NATURAL): BOOLEAN
      Result = (5<=n)

The function “is_five_or_more” has the type NATURAL?, i.e. it is a predicate
over natural numbers.

A predicate can have more than one argument. Predicates with more than one
argument can be used to define relations.

  [A,B,C]?     -- The total function [A,B,C]->BOOLEAN which describes
               -- a relation between the objects of type A, B and C

  [A,B]?       -- Binary relation between objects of type A and objects of
               -- type B

  [A,A]?       -- Binary relation between objects of the same type

The function “<=” is a predicate with two arguments of type NATURAL
(i.e. binary relation). It has the type [NATURAL,NATURAL]? and the following

  <= (a,b:NATURAL): ghost BOOLEAN
      Result = some(x:NATURAL) a + x = b

Note that if we have declared “<=” as a ghost predicate. In this case the
specification is sufficient. There is no need to give an actual

If we specified “<=” as a computable predicate (i.e. with result type BOOLEAN
instead of “ghost BOOLEAN”), the compiler would expect an implementation to
verify the computability of the predicate.

Higher order predicates

A predicate can have other predicates as arguments. Predicates over predicates
are called higher order predicates. E.g. we can define a first oder predicate

  is_even(n:NATURAL): BOOLEAN
      Result = (n mod 2 = 0)

which tells whether a natural number is even. The predicate “is_even” has type
NATURAL?. Instead of writing an explicit function to implement the predicate
we can use an anonymous function/predicate object as well. The predicate object

  (x:NATURAL) -> (n mod 2 = 0)

is equivalent to “is_even”.

The predicate “is_even” has some properties which can be described by higher
order predicates. E.g. we can define the higher order predicate

  is_even_prop_1(p:NATURAL?): ghost BOOLEAN
      Result = all(n:NATURAL) p[n] = (n mod 2 = 0)

The predicate “is_even_prop_1” has the type NATURAL??, i.e. it is a predicate
over predicates.

The predicate “is_even” (which is of type NATURAL?) satisfies this predicate
(which is of type NATURAL??), i.e. the assertions


  is_even_prop_1(x->(n mod 2 = 0))

are valid. All predicates which satisfy “is_even_prop_1” are equivalent to
“is_even”. Therefore “is_even_prop_1” can serve as a specification of

It is easy to find another predicate which is satisfied by “is_even”.

  is_even_prop_2(p:NATURAL?): ghost BOOLEAN
      Result = all(n:NATURAL) p[n] = some(m:NATURAL) 2*m = n

This predicate says that “p[n]” is true if and only if there is a natural
number “m” which satisfies “2*m=n”. “is_even_prop_2” is still a full
specification of the predicate “is_even”. I.e. all predicates satisfying
“is_even_spec_2” are equivalent to “is_even”.

In order to get a better feeling about what can be expressed by predicates
which can try to find some inductive properties of “is_even”. We know that the
number “0” is even and that the evenness of a number “n” implies the evenness
of “n+2”. This is expressed by the following predicate

  is_even_prop_3(p:NATURAL?): ghost BOOLEAN
      Result = (p[0] and all(n:NATURAL) p[n] => p[n+2])

It is evident that “is_even” satisfies “is_even_prop_3” i.e. the assertion


is valid. But not all predicates satisfying “is_even_prop_3” are equivalent to
“is_even”. A predicate which returns true for all natural number satisfies
“is_even_prop_3” as well i.e. we have the valid assertion


Therefore “is_even_prop_3” cannot be considered as a full specification of

However we feel that “is_even_prop_3” captures some essentials of
“is_even”. It is just not strong enough to be a full specification.

The module “predicate”

There is a module “predicate” which defines the base class and the basic
functions of predicates. The module “predicate” has an abstract class
PREDICATE[G]. All predicates of type T? inherit from the type PREDICATE[T].

  -- file: predicate.e
  immutable deferred class

The basic function is to ask whether an element satisfies a predicate

    [] (e:G): BOOLEAN
      deferred end

I.e. for a predicate “p:NATURAL?” the call “p[5]” returns whether the number
“5” satisfies the predicate “p”.

Since we can identify a predicate with the set of all values which satisfy the
predicate, all set operations like union, intersection, complement etc. have
their equivalent within the class predicate.

  feature   -- set operations
    or (f,g:CURRENT): CURRENT
        -- Union of the sets described by `f' and `g'.
        Result = x->(f[x] or g[x])

    and (f,g:CURRENT): CURRENT
        -- Intersection of the sets described by `f' and `g'.
        Result = x->(f[x] and g[x])

    not (f:CURRENT): CURRENT
        -- Complement of the set described by `f'.
        Result = x->(not f[x])

Note that the above function are computable functions and not ghost functions.

There are two predicate constants: One which cannot be satisfied by any object
and one which is satisfied by all objects.

  feature    -- Predicate constants
    False: CURRENT         -- overrides default type of "False"!
        Result = x->(False:BOOLEAN)  -- explicit type necessary here!

    True: CURRENT
        Result = x->(True:BOOLEAN)

In Modern Eiffel all constants (numeric constants, character constants, string
constants and boolean constants) can be used as names for constant functions
(i.e. 0-ary functions). In case of ambiguity the corresponding type has to be

  False               -- Boolean constant `False'
  False: CHARACTER?   -- Predicate over CHARACTERs which is false for all
                      -- arguments.

    a           := False          -- a has type BOOLEAN
    b: BOOLEAN  := True
    p: NATURAL? := False
    q           := True:STRING?   -- q has type STRING?

    d: BOOLEAN  := False:STRING?  -- ILLEGAL!! Type mismatch!!

The default type of the constants “True” and “False” is BOOLEAN. Within the
module “predicate” the default type is CURRENT (i.e. PREDICATE[G]). I.e. if we
want to use one of the constants within the module “predicate” with type
BOOLEAN, we have to specify the type explicitely.

Outside of the module “predicate” the constants “True” and “False” have their
default type. An explicit type has to be given in case that the default type
should be overridden.

  1. Leave a comment

Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

%d bloggers like this: