Go to the first, previous, next, last section, table of contents.

6.13 Specifying Higher-Order Functions

A higher-order function in C++ is a function that either takes pointers to functions as arguments, or returns them. A simple example is a sort function that takes a pointer to a comparison function as one of its arguments.

There Larch/C++ syntax that is used especially to specify higher-order functions is given below. See section 9.2 The Uses Clause for the syntax of trait-list.

higher-order-comparison ::= lsl-op-term satisfies fun-interface fun-spec-body
expects-clause ::= expects expected-trait-list
expected-trait-list ::= trait [ simple-id ] [ , trait [ simple-id ] ] ...
using-trait-list ::= using trait-or-deref-list
trait-or-deref-list ::= trait
              | * simple-id
              | trait-or-deref-list , trait
              | trait-or-deref-list , * simple-id

A higher-order-comparison is an equality-term (see section 6.1.3 Equality Terms and Quantifiers). It is used to check whether a C++ function, the lsl-op-term in the higher-order-comparison, satisfies a function specification. A higher-order-comparison has sort Bool.

An expects-clause is used to specify a theory that is needed to state the rest of the specification formal parameter must satisfy. This theory is typically used in the function-spec-body of a higher-order-comparison. To permit verification, code that calls a higher-order function must pass an actual parameter trait that contains the theory of each expected trait in the expects-clause. This is done using the form of a postfix-expression that Larch/C++ adds to C++ (see section 5.4.6 Function Declarations). The syntax is that, following the normal arguments, one can use the keyword using and then list either LSL traits or trait dereferences. These trait dereferences have the form * simple-id, where the simple-id is the name of a trait formal parameter. The named traits, and the values of the corresponding actual parameters for the dereferenced formals are passed, positionally. This is similar to the specification of generic functions and classes used in OBJ2 [Goguen84] and Resolve [Ernst-etal91] [Edwards-etal94]. See section 9.2 The Uses Clause for the exact syntax of trait.

To start with a standard kind of example, consider the function ArrayMap. This function takes an array, the array's length, and a pointer to a function, and modifies the array by applying the function to each element of the array, a[i], and placing the result of the call back in a[i]. It might be implemented as follows.

// this is C++ code, not a specification
typedef int (*int_fun)(int) throw();
void ArrayMap(int a[], int len, int_fun fun) {
  for (int i = 0; i < len; i++) {
    a[i] = (*fun)(a[i]);

To specify the ArrayMap function, one has to make some decisions, such as the following. Is this supposed to work when a is null or uninitialized? Is it supposed to work when the pointer fun is null or uninitialized? Does *fun to have to work for all integers? (If it does, then we are limiting the applicability of ArrayMap.) Do we care what happens if some a[i] does not satisfy the precondition of *fun? Do we care about overflow in the computation of a call to *fun? Can *fun have side-effects?

In the following specification, the first conjunct in the precondition requires a to be non-null and the relevant part to be initialized, the second conjunct requires fun to be non-null and initialized, and the fourth conjunct requires that each of the relevant elements of a satisfy the precondition of *fun. The third conjunct of ArrayMap's precondition is a higher-order-comparison. It is true just when (*fun)^ satisfies the function-spec-body in that conjunct. This is true if whenever x satisfies inDomain(x), then calling the function with argument x is guaranteed to terminate normally with a result that satisfies isResultFor(x, result) and is a legal int (due to inRange(result)).

// @(#)$Id: ArrayMap.lh,v 1.8 1998/08/29 20:13:22 leavens Exp $

typedef int (*int_fun)(int) throw();

extern void ArrayMap(int a[], int len, int_fun fun
                     /*@ expects NoSideEffectsFun(int, int) @*/) throw();
//@ behavior {
//@   requires assignedUpTo(a, len, pre) /\ assigned(fun, pre)
//@           /\ (*fun)^ satisfies
//@                        int ignored(int x) throw()
//@                        behavior {
//@                          requires inDomain(x);
//@                          ensures isResultFor(x, result)
//@                                  /\ inRange(result);
//@                        }
//@           /\ \forall i: int (between(0, i, len-1) => inDomain(a^[i]));
//@   modifies objectsUpTo(a, len);
//@   ensures \forall i: int (between(0, i, len-1)
//@                            => isResultFor(a^[i], a'[i]));
//@ }

The above example expects a trait parameter that implies the theory of NoSideEffectsFun(int, int), which is shown below. This trait specifies minimum requirements on the theory of the trait functions inDomain and isResultFor that are used in the function-spec-body that (*fun)^ must satisfy. Note, however, that the specification of the trait function isResultFor is not complete; this is typical for expected traits. A call to ArrayMap would provide an actual trait in a using-trait-list with a theory that contained the theory of this trait. For example, one might write the following to call ArrayMap

  ArrayMap(myArray, myArrayLen, myFun /*@ using myFunTrait @*/)

where myFunTrait is an actual parameter trait that specifies the trait functions inDomain and isResultFor required by NoSideEffectsFun(int, int). This actual parameter trait would typically provide a more precise specification of isResultFor.

[[[Should have a real example for the above.]]]

% @(#)$Id: NoSideEffectsFun.lsl,v 1.3 1995/12/24 02:21:35 leavens Exp $
% Domain and input/output predicates for a side-effect free
% programming language "function" (which may be nondeterministic).
NoSideEffectsFun(S, T): trait
    inDomain: S -> Bool
    isResultFor: S,T -> Bool
  asserts \forall s: S, t: T
    inDomain(s) => (\E t (isResultFor(s, t)));

As another example, consider a higher-order function ApplyTwice, which takes a pointer to a function and an integer and returns the result of applying the function twice, as in the following code.

// this is C++ code, not a specification
typedef int (*int_fun)(int);
int ApplyTwice(int_fun f, int i) {
  return f(f(i));

In the following specification, we have decided that the client can only count on the result provided the following conditions are met (as specified in the precondition). The pointer f must be non-null and initialized. The argument i must meet the precondition of *f, and must result in a value that again meets the precondition of f, and that f must be deterministic. Note that much of this information is not available in the code above, which only specifies how the computation is implemented, not what contract it fulfills.

// @(#)$Id: ApplyTwice.lh,v 1.15 1998/09/23 16:02:18 ruby Exp $

typedef int (*int_fun)(int) throw();

extern int ApplyTwice(int_fun f, int i
                     /*@ expects NoSideEffectsDetFun(int, int) @*/) throw();
//@ behavior {
//@   requires assigned(f, pre)
//@            /\ (*f)^ satisfies
//@                       int ignored(int j) throw()
//@                       behavior {
//@                         requires inDomain(j);
//@                         ensures result = resultFor(j) /\ inRange(result);
//@                       }
//@            /\ inDomain(i) /\ inDomain(resultFor(j));
//@   ensures result = resultFor(resultFor(j));
//@   ensures redundantly inRange(result);
//@   example \forall j: int (inDomain(j)
//@                           => (between(0, j, 30) /\ resultFor(j) = j+1))
//@           /\ i = 5 /\ result = 7;
//@ }

In the above specification, the example given supposes some additional properties of the trait functions inDomain and resultFor. Of course, the actual trait parameter might have different properties, but this indicates how knowing the actual parameter trait allows one to extract additional information from the postcondition.

The trait expected for the above example is built on the trait NoSideEffectsFun given above.

% @(#)$Id: NoSideEffectsDetFun.lsl,v 1.1 1995/12/24 02:23:32 leavens Exp $
% Domain, I/O relation, and result map for
% a side-effect free, deterministic programming language "function".
NoSideEffectsDetFun(S, T): trait
  includes NoSideEffectsFun(S, T)
    resultFor: S -> T
  asserts \forall e: S, r1,r2: T
    (inDomain(e) /\ isResultFor(e, r1) /\ isResultFor(e, r2))
      => r1 = r2;
    inDomain(e) => (isResultFor(e, resultFor(e)));

A common kind of higher-order function is a kind of iterator. Consider the following code for a C++ function, ArrayForEach. It applies f to each element of an array. In ArrayForEach, f is expected to have side-effects.

// this is C++ code, not a specification
typedef void (*elem_fun)(int) throw();
void ArrayForEach(int a[], int len, elem_fun f) {
  for (int i = 0; i < len; i++) {

In the following specification, of ArrayForEach, we try to allow as much freedom as possible to *f. That is, we allow *f to access global variables and to modify them (this allows one to use ArrayForEach to do output, or to sum the elements into a global), and even to trash them (this allows one to use ArrayForEach to decide what other memory to deallocate). To support arbitrary preconditions on the globals, and arbitrary postconditions, we pass the pre-state to the trait function inDomain, and we pass the pre- and post-states to isStateFor. However, we are careful not to allow *f to deallocate the part of a being used, and to not change its own location! In order to make it possible for *f not to change itself, we require that *f is not aliased to any of the a[i]. The postcondition says that the post-state is a possible state obtained from iterating the state change of *f, and also includes some other conclusions that follow from the inability of *f to change its own location, and to deallocate the part of a being used.

// @(#)$Id: ArrayForEach.lh,v 1.9 1998/08/29 21:48:52 leavens Exp $

typedef void (*elem_fun)(int) throw();

extern void ArrayForEach(int a[], int len, elem_fun f
                         /*@ expects SideEffectsFun(int) @*/) throw();
//@ behavior {
//@   uses ArrayIterateProc(Obj, int);

//@   requires assignedUpTo(a, len, pre) /\ assigned(f, pre)
//@            /\ (*f)^ satisfies
//@                       int ignored(int x) throw()
//@                       behavior {
//@                         extern everything;
//@                         requires inDomain(x,pre);
//@                         modifies everything;
//@                         trashes everything;
//@                         ensures isStateFor(x, pre, post)
//@                                /\ assignedUpTo(a, len, post)
//@                                /\ \forall i: int
//@                                       (between(0, i, len-1)
//@                                        => inDomain(a'[i], post))
//@                                /\ assigned(f, post) /\ unchanged(*f);
//@                       }
//@           /\ \forall i: int (between(0, i, len-1) => inDomain(a^[i])
//@                              /\ widen(*f) ~= widen(a[i]));

//@   modifies everything;
//@   trashes everything;

//@   ensures isIteratedStateFor(a, 0, len-1, pre, post)
//@           /\ assignedUpTo(a, len, post)
//@           /\ assigned(f, post) /\ unchanged(*f);
//@ }

The expected trait in the above specification is the following.

% @(#)$Id: SideEffectsFun.lsl,v 1.1 1995/12/24 22:09:32 leavens Exp $
% Domain and state relation predicates for a
% programming language procedure (which may be nondeterministic).
SideEffectsFun(T): trait
  includes State_Basics
    inDomain: T, State -> Bool
    isStateFor: T, State, State -> Bool
  asserts \forall e: T, pre, post: State
    inDomain(e, pre) => (\E post (isStateFor(e, pre, post)));

The specification of ArrayForEach also uses the following trait, which is not provided as a parameter.

% @(#)$Id: ArrayIterateProc.lsl,v 1.2 1995/12/24 22:25:22 leavens Exp $
% Iteration of state changes for elements of an array
ArrayIterateProc(Loc, Elem): trait
  assumes SideEffectsFun(Elem)
  includes Array(Loc, Elem)
    isIteratedStateFor: Arr[Loc[Elem]], int, int, State, State -> Bool
  asserts \forall a: Arr[Loc[Elem]], i,ub: int, pre,next,post: State
    (i >= ub)
      => isIteratedStateFor(a, i, ub, pre, pre);
    ((i < ub)
        /\ isStateFor(eval(a, pre)[i], pre, next)
        /\ isIteratedStateFor(a, i+1, ub, next, post))
      => isIteratedStateFor(a, i, ub, pre, post);

[[[More needs to be said about the formal semantics of the higher-order constructs. Should also give an example of a higher-order-comparison used in a postcondition.]]]

Go to the first, previous, next, last section, table of contents.