// @(#)$Id: array_add_one.lh,v 1.12 1997/06/03 20:29:57 leavens Exp $
extern void array_add_one(int ai[], int siz) throw();
//@ behavior {
//@   requires 0 <= siz /\ assignedUpTo(ai, siz)
//@        /\ \A i:int ((0 <= i /\ i <= (siz-1))
//@                      => (ai[i])^ + 1 <= INT_MAX);
//@   modifies ai;
//@   ensures \A i:int ((0 <= i /\ i <= (siz-1))
//@                      => (ai[i])' = (ai[i])^ + 1);
//@ }

[Index]

HTML generated using lcpp2html.