// @(#)$Id: widen4.lh,v 1.8 1998/08/27 22:56:53 leavens Exp $
extern void widen(int i) throw();
//@ behavior {
//@   extern int low_bound, high_bound;

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

//@   modifies low_bound, high_bound;

//@   ensures ((INT_MIN + i < low_bound^ /\ low_bound^ < high_bound^
//@                /\ high_bound^ < INT_MAX - i)
//@             => ((high_bound' - low_bound')
//@                      = (high_bound^ - low_bound^) + i
//@                /\ low_bound' <= low_bound^ /\ high_bound^ <= high_bound'))
//@        /\ ((INT_MIN + i >= low_bound^ /\ low_bound^ < high_bound^
//@                /\ high_bound^ < INT_MAX - i)
//@             => (high_bound' = high_bound^ + i /\ unchanged(low_bound)))
//@        /\ ((INT_MIN + i < low_bound^ /\ low_bound^ < high_bound^
//@                /\ high_bound^ >= INT_MAX - i)
//@             => (low_bound' = low_bound^ - i /\ unchanged(high_bound)));

//@   ensures redundantly inRange(low_bound') /\ inRange(high_bound');

//@   example 8 < INT_MAX /\ i = 2 /\ low_bound^ = 3 /\ high_bound^ = 6
//@                                /\ low_bound' = 1 /\ high_bound' = 6;
//@   example 8 < INT_MAX /\ i = 2 /\ low_bound^ = 3 /\ high_bound^ = 6
//@                                /\ low_bound' = 3 /\ high_bound' = 8;
//@   example 8 < INT_MAX /\ i = 2 /\ low_bound^ = 3 /\ high_bound^ = 6
//@                                /\ low_bound' = 2 /\ high_bound' = 7;
//@ }

[Index]

HTML generated using lcpp2html.