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 }