// @(#)$Id: widen2.lh,v 1.13 1997/06/03 20:30:27 leavens Exp $
extern void widen(int i) throw();
//@ behavior { // a desugared version of widen1
//@   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)
//@        \/ (assigned(low_bound, pre) /\ assigned(high_bound, pre)
//@                  /\ INT_MIN + i >= low_bound^ /\ low_bound^ < high_bound^
//@                  /\ high_bound^ < INT_MAX - i)
//@        \/ (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 ((assigned(low_bound, pre) /\ assigned(high_bound, pre)
//@                /\ 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'))
//@        /\ ((assigned(low_bound, pre) /\ assigned(high_bound, pre)
//@                /\ INT_MIN + i >= low_bound^ /\ low_bound^ < high_bound^
//@                /\ high_bound^ < INT_MAX - i)
//@            => (high_bound' = high_bound^ + i /\ unchanged(low_bound)))
//@        /\ ((assigned(low_bound, pre) /\ assigned(high_bound, pre)
//@                /\ INT_MIN + i < low_bound^ /\ low_bound^ < high_bound^
//@                /\ high_bound^ >= INT_MAX - i)
//@            => (low_bound' = low_bound^ - i /\ unchanged(high_bound)));
//@ }

[Index]

HTML generated using lcpp2html.