SourceForge.net LogoThe Eiffel Compiler / Interpreter (tecomp)

doc/papers/proof/predicates

Predicates, ghost predicates and higher order predicates

Motivation

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 again.

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
      ensure
          Result = (5<=n)
      end
 

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 definition.

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

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 implementation.

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
      ensure
          Result = (n mod 2 = 0)
      end
 

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".

  is_even_prop_1(p:NATURAL?): ghost BOOLEAN
      ensure
          Result = all(n:NATURAL) n in p = (n mod 2 = 0)
      end
 

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(is_even)
 
  is_even_prop_1({n: 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 "is_even".

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

  is_even_prop_2(p:NATURAL?): ghost BOOLEAN
    ensure
      Result = all(n:NATURAL) n in p = some(m:NATURAL) 2*m = n
    end
 

This predicate says that "n in p" 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
    ensure
      Result = (0 in p and all(n:NATURAL) p[n] => p[n+2])
    end
 

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

  is_even_prop_3(is_even)
 

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

  is_even_prop_3({x:True})
 

Therefore "is_even_prop_3" cannot be considered as a full specification of "is_even".

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 built in type PREDICATE. The class PREDICATE has a formal generic G which describes the elements of the set. The type T? is an abbreviation of the type PREDICATE[T].

  -- file: predicate.e
  immutable class
      PREDICATE[G]
  end
 

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

  feature
    in  (e:G, p:CURRENT): BOOLEAN
      note built_in end
  end
 

I.e. for a predicate "p:NATURAL?" the call "5 in p" 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
    + (f,g:CURRENT): CURRENT
            -- Union of the sets described by `f' and `g'.
        ensure
            Result = {x: x in f or x in g)
        end
 
    * (f,g:CURRENT): CURRENT
            -- Intersection of the sets described by `f' and `g'.
        ensure
            Result = {x: x in f and x in g)
        end
 
    - (f:CURRENT): CURRENT
            -- Complement of the set described by `f'.
        ensure
            Result = {x: not (x in f)}
        end
  end
 

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
      0: CURRENT
          ensure
              Result = {x: False}
          end
 
      1: CURRENT
          ensure
              Result = {x: True}
          end
  end
 

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 provided.

  0                   -- Number zero
  0: CHARACTER?       -- Predicate over CHARACTERs which is false for all
                      -- arguments.
 
  local
      a           := 0              -- a has type INTEGER
      b: INTEGER  := 0
      p: NATURAL? := 0
      q           := 0:STRING?      -- q has type STRING?
 
      d: INTEGER  := 0:STRING?      -- ILLEGAL!! Type mismatch!!
  then
      ...
  end
 

The default type of the constants "0" and "1" is INTEGER. 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 INTEGER, we have to specify the type explicitely.

Outside of the module "predicate" the constants "0" and "1" have their default type. An explicit type has to be given in case that the default type should be overridden.

Emacs suffix

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

- Motivation

- Basic definitions

- Higher order predicates

- The module "predicate"

- Emacs suffix


ip-location