// @(#)$Id: widen1.lh,v 1.10 1997/06/03 20:30:26 leavens Exp $
extern void widen(int i) throw();
//@ behavior {
//@   extern int low_bound, high_bound;

//@   // "normal" case
//@   requires assigned(low_bound, pre) /\ assigned(high_bound, pre)
//@            /\ INT_MIN + i < low_bound^ /\ low_bound^ < high_bound^
//@            /\ high_bound^ < INT_MAX - i;
//@   modifies low_bound, high_bound;
//@   ensures (high_bound' - low_bound') = (high_bound^ - low_bound^) + i
//@           /\ low_bound' <= low_bound^ /\ high_bound^ <= high_bound';
   
//@ also // other cases

//@   requires assigned(low_bound, pre) /\ assigned(high_bound, pre)
//@            /\ INT_MIN + i >= low_bound^ /\ low_bound^ < high_bound^
//@            /\ high_bound^ < INT_MAX - i;
//@   modifies high_bound;
//@   ensures high_bound' = high_bound^ + i;

//@ also

//@   requires assigned(low_bound, pre) /\ assigned(high_bound, pre)
//@            /\ INT_MIN + i < low_bound^ /\ low_bound^ < high_bound^
//@            /\ high_bound^ >= INT_MAX - i;
//@   modifies low_bound;
//@   ensures  low_bound' = low_bound^ - i;
//@ }

[Index]

HTML generated using lcpp2html.