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    }