    001    /* Copyright 2000, 2001, Compaq Computer Corporation */
    002
    003    package escjava.ast;
    004
    005    import javafe.ast.Expr;
    006    import javafe.ast.VariableAccess;
    007    import javafe.util.Location;
    008    import javafe.util.Assert;
    009
    010    /* @review kiniry - Why is this class not in hierarchy.j */
    011
    012    public class DecreasesInfo {
    013      // the location of the 'decreases' pragma
    014      public final int loc;
    015      //@ invariant loc != Location.NULL;
    016
    017      // the translated expression
    018      public final /*@ non_null */ Expr f;
    019
    020      // a local variable storing the previous value of expr "f"
    021      public final /*@ non_null */ VariableAccess fOld;
    022
    023      //@ requires loc != Location.NULL;
    024      public DecreasesInfo(int loc, /*@ non_null */ Expr f,
    025                           /*@ non_null */ VariableAccess fOld) {
    026        this.loc = loc;
    027        this.f = f;
    028        this.fOld = fOld;
    029      }
    030
    031      public void check() {
    032        Assert.notFalse(loc != Location.NULL &&
    033                        f != null && fOld != null);
    034      }
    035    }