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

[Index]

HTML generated using lcpp2html.