// @(#)$Id: present_bad.lh,v 1.9 1997/06/03 20:30:18 leavens Exp $
extern int present_bad(const int a[], int siz, int i) throw();
//@ behavior {
//@   requires 0 <= siz /\ assignedUpTo(a,siz);
//@   ensures result = (if (\E i:int (0 <= i /\ i < siz /\ (a[i])^ = i))
//@                     then i else -1);
//@ }

[Index]

HTML generated using lcpp2html.