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

[Index]

HTML generated using lcpp2html.