001    /* Copyright 2000, 2001, Compaq Computer Corporation */
002    
003    /* IF THIS IS A JAVA FILE, DO NOT EDIT IT!  
004    
005       Most Java files in this directory which are part of the Javafe AST
006       are automatically generated using the astgen comment (see
007       ESCTools/Javafe/astgen) from the input file 'hierarchy.h'.  If you
008       wish to modify AST classes or introduce new ones, modify
009       'hierarchy.j.'
010     */
011    
012    package javafe.ast;
013    
014    import javafe.util.Assert;
015    import javafe.util.Location;
016    import javafe.util.ErrorSet;
017    
018    // Convention: unless otherwise noted, integer fields named "loc" refer
019    // to the location of the first character of the syntactic unit
020    
021    
022    /**
023     * <code>ASTNode</code> is the root of the abstract syntax tree node
024     * hierarchy.  Every class representing a node in the AST is a (direct
025     * or indirect) subclass of this class.
026     *
027     * <p> In designing our AST classes, the following, broad approach was
028     * taken:
029     *
030     * <ul>
031     * 
032     * <li> <b>Design package javafe.ast to stand alone.</b>
033     * 
034     * <li> <b>Have a large, deep hierarchy, using the type system to
035     * encode many invariants.</b> (Used a program to generate boilerplate
036     * code, making it the large hierarchy more manageable.)
037     * 
038     * <li> <b>Represent children with public fields.</b>
039     * 
040     * <li> <b>Put most code outside AST classes.</b>
041     * 
042     * <li> <b>Support both switch-based and visitor-based traversal.</b>
043     * 
044     * <li> <b>Liberal use of locations.</b> AST classes contain location
045     * fields that indicate the corresponding part of the source program.
046     * 
047     * <li> <b>Use generic decorations.</b>
048     * 
049     * <li> <b>Rewrite tree to handle disambiguation.</b> Expression names
050     * and method names are ambiguous: the be of the form
051     * <i>package.type.members</i> or <i>type.members</i> or
052     * <i>local-variable.members</i> or even <i>members</i>.  The parser
053     * does not attempt to disambiguate among these, but rather generates
054     * either <code>ExprName</code> or <code>MethodName</code>.  A later
055     * pass replaces these nodes with either <code>VariableAccess</code>
056     * or concrete subclasses of <code>FieldAccess</code> or
057     * <code>MethodInvocation</code>.
058     * 
059     * <li> <b>Fill in fields and decorations to handle resolution.</b>
060     * The nodes that need to be resolved are: <code>TypeName</code>,
061     * <code>VariableAccess</code>, (three subclasses of)
062     * <code>FieldAccess</code>, (three subclasses of)
063     * <code>MethodInvocation</code>, <code>ConstructorInvocation</code>,
064     * and <code>NewInstanceExpr</code>.  All nodes except
065     * <code>TypeName</code> have a field named <code>decl</code> of the
066     * approriate type that is initialized to <code>null</code> and is
067     * filled in by name resolution.  For <code>TypeName</code> we use a
068     * decoration rather than a field to avoid a dependency on the
069     * <code>javafe.tc</code> package.
070     * 
071     * </ul>
072     * 
073     * <p> Measurements:
074     * <blockquote>
075     * Node abstract classes: 13
076     * <br> Node concrete classes: 59
077     * <br> Sequence classes: 12
078     * <br> Total classes: 84
079     * <br>
080     * <br> Input to code generator: 842 lines of code (513 excluding comments)
081     * <br> Code generator: 993 (675)
082     * <br> Total lines of code: 1835 (1188)
083     * <br> Output of code generator: 4298
084     * </blockquote>
085     * 
086     * <p> The complete list of subclasses is shown below.  The names of
087     * subclasses of this class correspond (in general) to the syntactic
088     * units that they represent.  Any exceptions to this rule are
089     * documented.  All non-leaf classes are abstract.  In parenthesis,
090     * the names and types of fields holding the locally-defined children
091     * classes are listed; a postfix <code>*</code> on a type indicates a
092     * sequence.  Square brackets indicate optional elements; the only
093     * these fields can be null.
094     * 
095     * <pre>
096     * ASTNode
097     *    CompilationUnit ([Name pkgName], [LexicalPragma* lexicalPragmas], ImportDecl* imports, TypeDecl* elems)
098     *    ImportDecl ()
099     *       SingleTypeImport (TypeName typeName)
100     *       OnDemandImport (Name pkgName)
101     *    TypeDecl (int modifiers, [ModifierPragma* pmodifiers], Identifier id, [TypeModifierPragma* tmodifiers], TypeName* superInterfaces, TypeDeclElem* elems)
102     *       ClassDecl ([TypeName superClass])
103     *       InterfaceDecl ()
104     *    TypeDeclElem () NOTE: This is an <em>interface</em>
105     *       TypeDecl
106     *       FieldDecl
107     *       RoutineDecl (int modifiers, [ModifierPragma* pmodifiers], FormalParaDecl* args, TypeName* raises, [BlockStmt body])
108     *          ConstructorDecl ([TypeModifierPragma* tmodifiers])
109     *          MethodDecl (Identifier id, Type returnType)
110     *       InitBlock (int modifiers, [ModifierPragma* pmodifiers], BlockStmt block)
111     *       TypeDeclElemPragma ()
112     *    GenericVarDecl (int modifiers, [ModifierPragma* pmodifiers], Identifier id, Type type)
113     *       LocalVarDecl ([VarInit init])
114     *       FieldDecl ([VarInit init])
115     *       FormalParaDecl ()
116     *    Stmt ()
117     *       GenericBlockStmt (Stmt* stmts)
118     *          BlockStmt ()
119     *          SwitchStmt (Expr expr)
120     *       AssertStmt (Expr expr, String l)
121     *       VarDeclStmt (LocalVarDecl decl)
122     *       ClassDeclStmt (ClassDecl anonDecl)
123     *       WhileStmt (Expr expr, Stmt stmt)
124     *       DoStmt (Expr expr, Stmt stmt)
125     *       SynchronizeStmt (Expr expr, BlockStmt stmt)
126     *       EvalStmt (Expr expr)
127     *       ReturnStmt ([Expr expr])
128     *       ThrowStmt (Expr expr)
129     *       BranchStmt ([Identifier label])
130     *          BreakStmt ()
131     *          ContinueStmt ()
132     *       LabelStmt (Identifier label, Stmt stmt)
133     *       IfStmt (Expr expr, Stmt thn, Stmt els)
134     *       ForStmt (Stmt* forInit, Expr test, Expr* forUpdate, Stmt body)
135     *       SkipStmt ()
136     *       SwitchLabel ([Expr expr])
137     *       TryFinallyStmt (Stmt tryClause, Stmt finallyClause)
138     *       TryCatchStmt (Stmt tryClause, CatchClause* catchClauses)
139     *       StmtPragma ()
140     *       ConstructorInvocation (boolean superCall, [Expr enclosingInstance], Expr* args)
141     *    CatchClause (FormalParaDecl arg, Stmt body)
142     *    VarInit ()
143     *       ArrayInit (VarInit* elems)
144     *       Expr ()
145     *          ThisExpr (Type classPrefix)
146     *          LiteralExpr (int tag, [Object value])
147     *          ArrayRefExpr (Expr array, Expr index)
148     *          NewInstanceExpr ([Expr enclosingInstance], TypeName type, Expr* args, [ClassDecl decl])
149     *          NewArrayExpr (Type type, Expr* dims, [ArrayInit init])
150     *          CondExpr (Expr test, Expr thn, Expr els)
151     *          InstanceOfExpr (Expr expr, Type type)
152     *          CastExpr (Expr expr, Type type)
153     *          BinaryExpr (int op, Expr left, Expr right)
154     *          UnaryExpr (int op, Expr expr)
155     *          ParenExpr (Expr expr)
156     *          AmbiguousVariableAccess (Name name)
157     *          VariableAccess (Identifier id)
158     *          FieldAccess (ObjectDesignator od, Identifier id)
159     *          AmbiguousMethodInvocation (Name name, Expr* args)
160     *          MethodInvocation (ObjectDesignator od, Identifier id, Expr* args)
161     *          ClassLiteral (Type type)
162     *    ObjectDesignator ()  // "expr.", "type." or "super."
163     *       ExprObjectDesignator (Expr expr)
164     *       TypeObjectDesignator (Type type)
165     *       SuperObjectDesignator ()
166     *    Type ()
167     *       ErrorType() // was previously represented as a PrimitiveType
168     *       PrimitiveType (int tag)
169     *       TypeName (Name name)
170     *       ArrayType (Type elemType)
171     *    Name ()
172     *       SimpleName (Identifier id)
173     *       CompoundName (Identifier* ids)
174     *    ModifierPragma ()
175     *    LexicalPragma ()
176     *    TypeModifierPragma ()
177     * </pre>
178     */
179    
180    public abstract class ASTNode implements Cloneable
181    {
182      /**
183       * The decorations that have been attached to this node.  This is a
184       * package-level field accessed by the <code>ASTDecoration</code>
185       * class.  There are different ways to implement decorations; this
186       * way is not space-efficient, but it's pretty fast.
187       */
188    
189      //@ invariant decorations != null ==> (\typeof(decorations) == \type(Object[]));
190      Object[] decorations;  
191    
192      //@ ensures !(this instanceof  Type) ==> \result != Location.NULL;
193      /*@ ensures (this instanceof Type) ==>
194                     ((Type)this).syntax ==> (\result != Location.NULL); */
195      public abstract int getStartLoc();
196    
197      //@ ensures !(this instanceof  Type) ==> \result != Location.NULL;
198      /*@ ensures (this instanceof Type) ==>
199                     ((Type)this).syntax ==> (\result != Location.NULL); */
200      public int getEndLoc() { 
201        int start = getStartLoc();
202        if( start == Location.NULL )
203          return Location.NULL;
204        else
205          return start;
206      }
207    
208      //@ ensures \result != null;
209      //@ ensures \typeof(\result) == \typeof(this);
210      //@ ensures \result.owner == null;
211      public Object clone(boolean b)  {
212        ASTNode n = null;
213        try {
214          n = (ASTNode)super.clone();
215          if (!b) {
216            n.decorations = null;
217          }
218        } catch(java.lang.CloneNotSupportedException e) {
219          ErrorSet.fatal("Internal error in AST hierarchy: no clone");
220          n = this; // dummy assingment to appease escjava.
221        }
222        return n;
223      }
224     
225      /**
226       * Clone node, where the clone has the same decorations as original.
227       */
228      public Object clone() {
229        return clone(true);
230      }
231      
232      public Object[] getDecorations() {
233        return decorations;
234      }
235    
236      //@ requires d != null ==> \typeof(d) == \type(Object[]);
237      public void setDecorations(Object d[]) {
238        decorations = d;
239      }
240      
241      /**
242       * Used to remind callers of ASTNode subclass constructors that they
243       * must manually establish any required invariants after calling an
244       * AST constructor.  (AST constructors do not establish any class
245       * invariants.)
246       */
247      //@ ghost public static boolean I_will_establish_invariants_afterwards;
248    
249    
250    // Generated boilerplate constructors:
251    
252       /**
253        * Construct a raw ASTNode whose class invariant(s) have not
254        * yet been established.  It is the caller's job to
255        * initialize the returned node's fields so that any
256        * class invariants hold.
257        */
258       //@ requires I_will_establish_invariants_afterwards;
259       protected ASTNode() {}    //@ nowarn Invariant,NonNullInit;
260    
261       
262    
263    // Generated boilerplate methods:
264    
265       /** Return the number of children a node has. */
266       //@ ensures \result >= 0;
267       public abstract int childCount();
268    
269       /** Return the first-but-ith child of a node. */
270       //@ requires 0 <= i;
271       public abstract Object childAt(int i);
272    
273       /** Return the tag of a node. */
274      //@ ensures (this instanceof LiteralExpr) ==> \result==((LiteralExpr)this).tag;
275      //@ ensures (this instanceof BinaryExpr) ==> \result==((BinaryExpr)this).op;
276      //@ ensures (this instanceof UnaryExpr) ==> \result==((UnaryExpr)this).op;
277      //@ ensures (this instanceof PrimitiveType) ==>\result==((PrimitiveType)this).tag;
278      //
279      //@ ensures (\result==javafe.tc.TagConstants.TYPESIG) ==> \typeof(this) <: \type(javafe.tc.TypeSig);
280      //
281      // Remaining part of spec is automatically generated:
282      //@ ensures (\result==TagConstants.COMPILATIONUNIT) ==> \typeof(this) <: \type(javafe.ast.CompilationUnit);
283      //@ ensures (\result==TagConstants.SINGLETYPEIMPORTDECL) ==> \typeof(this) <: \type(javafe.ast.SingleTypeImportDecl);
284      //@ ensures (\result==TagConstants.ONDEMANDIMPORTDECL) ==> \typeof(this) <: \type(javafe.ast.OnDemandImportDecl);
285      //@ ensures (\result==TagConstants.CLASSDECL) ==> \typeof(this) <: \type(javafe.ast.ClassDecl);
286      //@ ensures (\result==TagConstants.INTERFACEDECL) ==> \typeof(this) <: \type(javafe.ast.InterfaceDecl);
287      //@ ensures (\result==TagConstants.CONSTRUCTORDECL) ==> \typeof(this) <: \type(javafe.ast.ConstructorDecl);
288      //@ ensures (\result==TagConstants.METHODDECL) ==> \typeof(this) <: \type(javafe.ast.MethodDecl);
289      //@ ensures (\result==TagConstants.INITBLOCK) ==> \typeof(this) <: \type(javafe.ast.InitBlock);
290      //@ ensures (\result==TagConstants.LOCALVARDECL) ==> \typeof(this) <: \type(javafe.ast.LocalVarDecl);
291      //@ ensures (\result==TagConstants.FIELDDECL) ==> \typeof(this) <: \type(javafe.ast.FieldDecl);
292      //@ ensures (\result==TagConstants.FORMALPARADECL) ==> \typeof(this) <: \type(javafe.ast.FormalParaDecl);
293      //@ ensures (\result==TagConstants.BLOCKSTMT) ==> \typeof(this) <: \type(javafe.ast.BlockStmt);
294      //@ ensures (\result==TagConstants.SWITCHSTMT) ==> \typeof(this) <: \type(javafe.ast.SwitchStmt);
295      //@ ensures (\result==TagConstants.ASSERTSTMT) ==> \typeof(this) <: \type(javafe.ast.AssertStmt);
296      //@ ensures (\result==TagConstants.VARDECLSTMT) ==> \typeof(this) <: \type(javafe.ast.VarDeclStmt);
297      //@ ensures (\result==TagConstants.CLASSDECLSTMT) ==> \typeof(this) <: \type(javafe.ast.ClassDeclStmt);
298      //@ ensures (\result==TagConstants.WHILESTMT) ==> \typeof(this) <: \type(javafe.ast.WhileStmt);
299      //@ ensures (\result==TagConstants.DOSTMT) ==> \typeof(this) <: \type(javafe.ast.DoStmt);
300      //@ ensures (\result==TagConstants.SYNCHRONIZESTMT) ==> \typeof(this) <: \type(javafe.ast.SynchronizeStmt);
301      //@ ensures (\result==TagConstants.EVALSTMT) ==> \typeof(this) <: \type(javafe.ast.EvalStmt);
302      //@ ensures (\result==TagConstants.RETURNSTMT) ==> \typeof(this) <: \type(javafe.ast.ReturnStmt);
303      //@ ensures (\result==TagConstants.THROWSTMT) ==> \typeof(this) <: \type(javafe.ast.ThrowStmt);
304      //@ ensures (\result==TagConstants.BREAKSTMT) ==> \typeof(this) <: \type(javafe.ast.BreakStmt);
305      //@ ensures (\result==TagConstants.CONTINUESTMT) ==> \typeof(this) <: \type(javafe.ast.ContinueStmt);
306      //@ ensures (\result==TagConstants.LABELSTMT) ==> \typeof(this) <: \type(javafe.ast.LabelStmt);
307      //@ ensures (\result==TagConstants.IFSTMT) ==> \typeof(this) <: \type(javafe.ast.IfStmt);
308      //@ ensures (\result==TagConstants.FORSTMT) ==> \typeof(this) <: \type(javafe.ast.ForStmt);
309      //@ ensures (\result==TagConstants.SKIPSTMT) ==> \typeof(this) <: \type(javafe.ast.SkipStmt);
310      //@ ensures (\result==TagConstants.SWITCHLABEL) ==> \typeof(this) <: \type(javafe.ast.SwitchLabel);
311      //@ ensures (\result==TagConstants.TRYFINALLYSTMT) ==> \typeof(this) <: \type(javafe.ast.TryFinallyStmt);
312      //@ ensures (\result==TagConstants.TRYCATCHSTMT) ==> \typeof(this) <: \type(javafe.ast.TryCatchStmt);
313      //@ ensures (\result==TagConstants.CONSTRUCTORINVOCATION) ==> \typeof(this) <: \type(javafe.ast.ConstructorInvocation);
314      //@ ensures (\result==TagConstants.CATCHCLAUSE) ==> \typeof(this) <: \type(javafe.ast.CatchClause);
315      //@ ensures (\result==TagConstants.ARRAYINIT) ==> \typeof(this) <: \type(javafe.ast.ArrayInit);
316      //@ ensures (\result==TagConstants.THISEXPR) ==> \typeof(this) <: \type(javafe.ast.ThisExpr);
317      //@ ensures (\result==TagConstants.ARRAYREFEXPR) ==> \typeof(this) <: \type(javafe.ast.ArrayRefExpr);
318      //@ ensures (\result==TagConstants.NEWINSTANCEEXPR) ==> \typeof(this) <: \type(javafe.ast.NewInstanceExpr);
319      //@ ensures (\result==TagConstants.NEWARRAYEXPR) ==> \typeof(this) <: \type(javafe.ast.NewArrayExpr);
320      //@ ensures (\result==TagConstants.CONDEXPR) ==> \typeof(this) <: \type(javafe.ast.CondExpr);
321      //@ ensures (\result==TagConstants.INSTANCEOFEXPR) ==> \typeof(this) <: \type(javafe.ast.InstanceOfExpr);
322      //@ ensures (\result==TagConstants.CASTEXPR) ==> \typeof(this) <: \type(javafe.ast.CastExpr);
323      //@ ensures (\result==TagConstants.PARENEXPR) ==> \typeof(this) <: \type(javafe.ast.ParenExpr);
324      //@ ensures (\result==TagConstants.AMBIGUOUSVARIABLEACCESS) ==> \typeof(this) <: \type(javafe.ast.AmbiguousVariableAccess);
325      //@ ensures (\result==TagConstants.VARIABLEACCESS) ==> \typeof(this) <: \type(javafe.ast.VariableAccess);
326      //@ ensures (\result==TagConstants.FIELDACCESS) ==> \typeof(this) <: \type(javafe.ast.FieldAccess);
327      //@ ensures (\result==TagConstants.AMBIGUOUSMETHODINVOCATION) ==> \typeof(this) <: \type(javafe.ast.AmbiguousMethodInvocation);
328      //@ ensures (\result==TagConstants.METHODINVOCATION) ==> \typeof(this) <: \type(javafe.ast.MethodInvocation);
329      //@ ensures (\result==TagConstants.CLASSLITERAL) ==> \typeof(this) <: \type(javafe.ast.ClassLiteral);
330      //@ ensures (\result==TagConstants.EXPROBJECTDESIGNATOR) ==> \typeof(this) <: \type(javafe.ast.ExprObjectDesignator);
331      //@ ensures (\result==TagConstants.TYPEOBJECTDESIGNATOR) ==> \typeof(this) <: \type(javafe.ast.TypeObjectDesignator);
332      //@ ensures (\result==TagConstants.SUPEROBJECTDESIGNATOR) ==> \typeof(this) <: \type(javafe.ast.SuperObjectDesignator);
333      //@ ensures (\result==TagConstants.ERRORTYPE) ==> \typeof(this) <: \type(javafe.ast.ErrorType);
334      //@ ensures (\result==TagConstants.TYPENAME) ==> \typeof(this) <: \type(javafe.ast.TypeName);
335      //@ ensures (\result==TagConstants.ARRAYTYPE) ==> \typeof(this) <: \type(javafe.ast.ArrayType);
336      //@ ensures (\result==TagConstants.SIMPLENAME) ==> \typeof(this) <: \type(javafe.ast.SimpleName);
337      //@ ensures (\result==TagConstants.COMPOUNDNAME) ==> \typeof(this) <: \type(javafe.ast.CompoundName);
338      //@ ensures (\result==TagConstants.OR) ==> \typeof(this) <: \type(javafe.ast.BinaryExpr);
339      //@ ensures (\result==TagConstants.AND) ==> \typeof(this) <: \type(javafe.ast.BinaryExpr);
340      //@ ensures (\result==TagConstants.BITOR) ==> \typeof(this) <: \type(javafe.ast.BinaryExpr);
341      //@ ensures (\result==TagConstants.BITXOR) ==> \typeof(this) <: \type(javafe.ast.BinaryExpr);
342      //@ ensures (\result==TagConstants.BITAND) ==> \typeof(this) <: \type(javafe.ast.BinaryExpr);
343      //@ ensures (\result==TagConstants.NE) ==> \typeof(this) <: \type(javafe.ast.BinaryExpr);
344      //@ ensures (\result==TagConstants.EQ) ==> \typeof(this) <: \type(javafe.ast.BinaryExpr);
345      //@ ensures (\result==TagConstants.GE) ==> \typeof(this) <: \type(javafe.ast.BinaryExpr);
346      //@ ensures (\result==TagConstants.GT) ==> \typeof(this) <: \type(javafe.ast.BinaryExpr);
347      //@ ensures (\result==TagConstants.LE) ==> \typeof(this) <: \type(javafe.ast.BinaryExpr);
348      //@ ensures (\result==TagConstants.LT) ==> \typeof(this) <: \type(javafe.ast.BinaryExpr);
349      //@ ensures (\result==TagConstants.LSHIFT) ==> \typeof(this) <: \type(javafe.ast.BinaryExpr);
350      //@ ensures (\result==TagConstants.RSHIFT) ==> \typeof(this) <: \type(javafe.ast.BinaryExpr);
351      //@ ensures (\result==TagConstants.URSHIFT) ==> \typeof(this) <: \type(javafe.ast.BinaryExpr);
352      //@ ensures (\result==TagConstants.ADD) ==> \typeof(this) <: \type(javafe.ast.BinaryExpr);
353      //@ ensures (\result==TagConstants.SUB) ==> \typeof(this) <: \type(javafe.ast.BinaryExpr);
354      //@ ensures (\result==TagConstants.DIV) ==> \typeof(this) <: \type(javafe.ast.BinaryExpr);
355      //@ ensures (\result==TagConstants.MOD) ==> \typeof(this) <: \type(javafe.ast.BinaryExpr);
356      //@ ensures (\result==TagConstants.STAR) ==> \typeof(this) <: \type(javafe.ast.BinaryExpr);
357      //@ ensures (\result==TagConstants.ASSIGN) ==> \typeof(this) <: \type(javafe.ast.BinaryExpr);
358      //@ ensures (\result==TagConstants.ASGMUL) ==> \typeof(this) <: \type(javafe.ast.BinaryExpr);
359      //@ ensures (\result==TagConstants.ASGDIV) ==> \typeof(this) <: \type(javafe.ast.BinaryExpr);
360      //@ ensures (\result==TagConstants.ASGREM) ==> \typeof(this) <: \type(javafe.ast.BinaryExpr);
361      //@ ensures (\result==TagConstants.ASGADD) ==> \typeof(this) <: \type(javafe.ast.BinaryExpr);
362      //@ ensures (\result==TagConstants.ASGSUB) ==> \typeof(this) <: \type(javafe.ast.BinaryExpr);
363      //@ ensures (\result==TagConstants.ASGLSHIFT) ==> \typeof(this) <: \type(javafe.ast.BinaryExpr);
364      //@ ensures (\result==TagConstants.ASGRSHIFT) ==> \typeof(this) <: \type(javafe.ast.BinaryExpr);
365      //@ ensures (\result==TagConstants.ASGURSHIFT) ==> \typeof(this) <: \type(javafe.ast.BinaryExpr);
366      //@ ensures (\result==TagConstants.ASGBITAND) ==> \typeof(this) <: \type(javafe.ast.BinaryExpr);
367      //@ ensures (\result==TagConstants.ASGBITOR) ==> \typeof(this) <: \type(javafe.ast.BinaryExpr);
368      //@ ensures (\result==TagConstants.ASGBITXOR) ==> \typeof(this) <: \type(javafe.ast.BinaryExpr);
369      //@ ensures (\result==TagConstants.UNARYADD) ==> \typeof(this) <: \type(javafe.ast.UnaryExpr);
370      //@ ensures (\result==TagConstants.UNARYSUB) ==> \typeof(this) <: \type(javafe.ast.UnaryExpr);
371      //@ ensures (\result==TagConstants.NOT) ==> \typeof(this) <: \type(javafe.ast.UnaryExpr);
372      //@ ensures (\result==TagConstants.BITNOT) ==> \typeof(this) <: \type(javafe.ast.UnaryExpr);
373      //@ ensures (\result==TagConstants.INC) ==> \typeof(this) <: \type(javafe.ast.UnaryExpr);
374      //@ ensures (\result==TagConstants.DEC) ==> \typeof(this) <: \type(javafe.ast.UnaryExpr);
375      //@ ensures (\result==TagConstants.POSTFIXINC) ==> \typeof(this) <: \type(javafe.ast.UnaryExpr);
376      //@ ensures (\result==TagConstants.POSTFIXDEC) ==> \typeof(this) <: \type(javafe.ast.UnaryExpr);
377      //@ ensures (\result==TagConstants.BOOLEANTYPE) ==> \typeof(this) <: \type(javafe.ast.PrimitiveType);
378      //@ ensures (\result==TagConstants.INTTYPE) ==> \typeof(this) <: \type(javafe.ast.PrimitiveType);
379      //@ ensures (\result==TagConstants.LONGTYPE) ==> \typeof(this) <: \type(javafe.ast.PrimitiveType);
380      //@ ensures (\result==TagConstants.CHARTYPE) ==> \typeof(this) <: \type(javafe.ast.PrimitiveType);
381      //@ ensures (\result==TagConstants.FLOATTYPE) ==> \typeof(this) <: \type(javafe.ast.PrimitiveType);
382      //@ ensures (\result==TagConstants.DOUBLETYPE) ==> \typeof(this) <: \type(javafe.ast.PrimitiveType);
383      //@ ensures (\result==TagConstants.VOIDTYPE) ==> \typeof(this) <: \type(javafe.ast.PrimitiveType);
384      //@ ensures (\result==TagConstants.NULLTYPE) ==> \typeof(this) <: \type(javafe.ast.PrimitiveType);
385      //@ ensures (\result==TagConstants.BYTETYPE) ==> \typeof(this) <: \type(javafe.ast.PrimitiveType);
386      //@ ensures (\result==TagConstants.SHORTTYPE) ==> \typeof(this) <: \type(javafe.ast.PrimitiveType);
387      //@ ensures (\result==TagConstants.BOOLEANLIT) ==> \typeof(this) <: \type(javafe.ast.LiteralExpr);
388      //@ ensures (\result==TagConstants.INTLIT) ==> \typeof(this) <: \type(javafe.ast.LiteralExpr);
389      //@ ensures (\result==TagConstants.LONGLIT) ==> \typeof(this) <: \type(javafe.ast.LiteralExpr);
390      //@ ensures (\result==TagConstants.CHARLIT) ==> \typeof(this) <: \type(javafe.ast.LiteralExpr);
391      //@ ensures (\result==TagConstants.FLOATLIT) ==> \typeof(this) <: \type(javafe.ast.LiteralExpr);
392      //@ ensures (\result==TagConstants.DOUBLELIT) ==> \typeof(this) <: \type(javafe.ast.LiteralExpr);
393      //@ ensures (\result==TagConstants.STRINGLIT) ==> \typeof(this) <: \type(javafe.ast.LiteralExpr);
394      //@ ensures (\result==TagConstants.NULLLIT) ==> \typeof(this) <: \type(javafe.ast.LiteralExpr);
395       public abstract int getTag();
396    
397       /** Return a string representation of <code>this</code>.
398       Meant for debugging use only, not for presentation. */
399       public abstract String toString();
400    
401       /** Accept a visit from <code>v</code>.  This method simply
402       calls the method of <code>v</code> corresponding to the
403       allocated type of <code>this</code>, passing <code>this</code>
404       as the argument.  See the design patterns book. */
405       //@ requires v != null;
406       public abstract void accept(Visitor v);
407    
408       //@ requires v != null;
409    //@ ensures \result != null;
410    public abstract Object accept(VisitorArgResult v, Object o);
411    
412       public void check() {
413       }
414    
415    }