// @(#)$Id: widen3.lh,v 1.6 1998/08/27 22:56:52 leavens Exp $
extern void widen(int i) throw();
//@ behavior {
//@   extern int low_bound, high_bound;
//@
//@   let lb: Obj[int] be low_bound, hb: Obj[int] be high_bound;
//@   requires assigned(lb, pre) /\ assigned(hb, pre);
//@   {
//@      requires INT_MIN + i < lb^ /\ lb^ < hb^ /\ hb^ < INT_MAX - i;
//@      modifies lb, hb;
//@      ensures (hb' - lb') = (hb^ - lb^) + i /\ lb' <= lb^ /\ hb^ <= hb';
//@   
//@    also // other cases
//@
//@      requires INT_MIN + i >= lb^ /\ lb^ < hb^ /\ hb^ < INT_MAX - i;
//@      modifies hb;
//@      ensures hb' = hb^ + i;
//@
//@    also
//@
//@      requires INT_MIN + i < lb^ /\ lb^ < hb^ /\ hb^ >= INT_MAX - i;
//@      modifies lb;
//@      ensures  lb' = lb^ - i;
//@   }
//@   ensures redundantly inRange(lb') /\ inRange(hb');
//@   example 8 < INT_MAX /\ i = 2 /\ lb^ = 3 /\ hb^ = 6
//@                                /\ lb' = 1 /\ hb' = 6;
//@   example 8 < INT_MAX /\ i = 2 /\ lb^ = 3 /\ hb^ = 6
//@                                /\ lb' = 3 /\ hb' = 8;
//@   example 8 < INT_MAX /\ i = 2 /\ lb^ = 3 /\ hb^ = 6
//@                                /\ lb' = 2 /\ hb' = 7;
//@ }

[Index]

HTML generated using lcpp2html.