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-termsatisfiesfun-interface fun-spec-body expects-clause ::=expectsexpected-trait-list expected-trait-list ::= trait [ simple-id ] [,trait [ simple-id ] ] ... using-trait-list ::=usingtrait-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
introduces
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)
introduces
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++) {
(*f)(a[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
introduces
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)
introduces
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.