/* This class is correct in a single-threaded context, but not a
 * multithreaded one. */

public class RangeSeqOK {
    private int lower;
    private int upper;
    // INVARIANT: lower <= upper
    private boolean invariantOK(int l, int u) {
	return l <= u;
    }
    public RangeSeqOK(int lower, int upper) throws IllegalArgumentException {
	if (!invariantOK(lower,upper)) 
	    throw new IllegalArgumentException();
	this.lower = lower;
	this.upper = upper;
    }
    public boolean inRange(int v) {
	if (v >= lower && v <= upper) return true;
	return false;
    }
    public void incUpper() {
	upper ++; // assumes no overflow
    }
    public void incLower() throws IllegalArgumentException {
	if (!invariantOK(lower+1,upper)) 
	    throw new IllegalArgumentException();
	lower ++;
    }
    public void decLower() {
	lower-- ; // assumes no underflow
    }
    public void decUpper() throws IllegalArgumentException {
	if (!invariantOK(lower,upper-1)) 
	    throw new IllegalArgumentException();
	upper --;
    }
}