// @(#)$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]));
//@ }

[Index]

HTML generated using lcpp2html.