    001    package javafe.ast;
    002
    003
    004    /**
    005     ** Represents either a ClassBodyDeclaration or an
    006     ** InterfaceMemberDeclaration.
    007     **/
    008
    009    public interface TypeDeclElem {
    010
    011        /** Return the tag of a node. */
    012      //@ ensures (this instanceof LiteralExpr) ==> \result==((LiteralExpr)this).tag;
    013      //@ ensures (this instanceof BinaryExpr) ==> \result==((BinaryExpr)this).op;
    014      //@ ensures (this instanceof UnaryExpr) ==> \result==((UnaryExpr)this).op;
    015      //@ ensures (this instanceof PrimitiveType) ==>\result==((PrimitiveType)this).tag;
    016      //
    017      //@ ensures (\result==javafe.tc.TagConstants.TYPESIG) ==> \typeof(this) <: \type(javafe.tc.TypeSig);
    018      //
    019      // Remaining part of spec is automatically generated:
    020      //@ ensures (\result==TagConstants.COMPILATIONUNIT) ==> \typeof(this) <: \type(javafe.ast.CompilationUnit);
    021      //@ ensures (\result==TagConstants.SINGLETYPEIMPORTDECL) ==> \typeof(this) <: \type(javafe.ast.SingleTypeImportDecl);
    022      //@ ensures (\result==TagConstants.ONDEMANDIMPORTDECL) ==> \typeof(this) <: \type(javafe.ast.OnDemandImportDecl);
    023      //@ ensures (\result==TagConstants.CLASSDECL) ==> \typeof(this) <: \type(javafe.ast.ClassDecl);
    024      //@ ensures (\result==TagConstants.INTERFACEDECL) ==> \typeof(this) <: \type(javafe.ast.InterfaceDecl);
    025      //@ ensures (\result==TagConstants.CONSTRUCTORDECL) ==> \typeof(this) <: \type(javafe.ast.ConstructorDecl);
    026      //@ ensures (\result==TagConstants.METHODDECL) ==> \typeof(this) <: \type(javafe.ast.MethodDecl);
    027      //@ ensures (\result==TagConstants.INITBLOCK) ==> \typeof(this) <: \type(javafe.ast.InitBlock);
    028      //@ ensures (\result==TagConstants.LOCALVARDECL) ==> \typeof(this) <: \type(javafe.ast.LocalVarDecl);
    029      //@ ensures (\result==TagConstants.FIELDDECL) ==> \typeof(this) <: \type(javafe.ast.FieldDecl);
    030      //@ ensures (\result==TagConstants.FORMALPARADECL) ==> \typeof(this) <: \type(javafe.ast.FormalParaDecl);
    031      //@ ensures (\result==TagConstants.BLOCKSTMT) ==> \typeof(this) <: \type(javafe.ast.BlockStmt);
    032      //@ ensures (\result==TagConstants.SWITCHSTMT) ==> \typeof(this) <: \type(javafe.ast.SwitchStmt);
    033      //@ ensures (\result==TagConstants.ASSERTSTMT) ==> \typeof(this) <: \type(javafe.ast.AssertStmt);
    034      //@ ensures (\result==TagConstants.VARDECLSTMT) ==> \typeof(this) <: \type(javafe.ast.VarDeclStmt);
    035      //@ ensures (\result==TagConstants.CLASSDECLSTMT) ==> \typeof(this) <: \type(javafe.ast.ClassDeclStmt);
    036      //@ ensures (\result==TagConstants.WHILESTMT) ==> \typeof(this) <: \type(javafe.ast.WhileStmt);
    037      //@ ensures (\result==TagConstants.DOSTMT) ==> \typeof(this) <: \type(javafe.ast.DoStmt);
    038      //@ ensures (\result==TagConstants.SYNCHRONIZESTMT) ==> \typeof(this) <: \type(javafe.ast.SynchronizeStmt);
    039      //@ ensures (\result==TagConstants.EVALSTMT) ==> \typeof(this) <: \type(javafe.ast.EvalStmt);
    040      //@ ensures (\result==TagConstants.RETURNSTMT) ==> \typeof(this) <: \type(javafe.ast.ReturnStmt);
    041      //@ ensures (\result==TagConstants.THROWSTMT) ==> \typeof(this) <: \type(javafe.ast.ThrowStmt);
    042      //@ ensures (\result==TagConstants.BREAKSTMT) ==> \typeof(this) <: \type(javafe.ast.BreakStmt);
    043      //@ ensures (\result==TagConstants.CONTINUESTMT) ==> \typeof(this) <: \type(javafe.ast.ContinueStmt);
    044      //@ ensures (\result==TagConstants.LABELSTMT) ==> \typeof(this) <: \type(javafe.ast.LabelStmt);
    045      //@ ensures (\result==TagConstants.IFSTMT) ==> \typeof(this) <: \type(javafe.ast.IfStmt);
    046      //@ ensures (\result==TagConstants.FORSTMT) ==> \typeof(this) <: \type(javafe.ast.ForStmt);
    047      //@ ensures (\result==TagConstants.SKIPSTMT) ==> \typeof(this) <: \type(javafe.ast.SkipStmt);
    048      //@ ensures (\result==TagConstants.SWITCHLABEL) ==> \typeof(this) <: \type(javafe.ast.SwitchLabel);
    049      //@ ensures (\result==TagConstants.TRYFINALLYSTMT) ==> \typeof(this) <: \type(javafe.ast.TryFinallyStmt);
    050      //@ ensures (\result==TagConstants.TRYCATCHSTMT) ==> \typeof(this) <: \type(javafe.ast.TryCatchStmt);
    051      //@ ensures (\result==TagConstants.CONSTRUCTORINVOCATION) ==> \typeof(this) <: \type(javafe.ast.ConstructorInvocation);
    052      //@ ensures (\result==TagConstants.CATCHCLAUSE) ==> \typeof(this) <: \type(javafe.ast.CatchClause);
    053      //@ ensures (\result==TagConstants.ARRAYINIT) ==> \typeof(this) <: \type(javafe.ast.ArrayInit);
    054      //@ ensures (\result==TagConstants.THISEXPR) ==> \typeof(this) <: \type(javafe.ast.ThisExpr);
    055      //@ ensures (\result==TagConstants.ARRAYREFEXPR) ==> \typeof(this) <: \type(javafe.ast.ArrayRefExpr);
    056      //@ ensures (\result==TagConstants.NEWINSTANCEEXPR) ==> \typeof(this) <: \type(javafe.ast.NewInstanceExpr);
    057      //@ ensures (\result==TagConstants.NEWARRAYEXPR) ==> \typeof(this) <: \type(javafe.ast.NewArrayExpr);
    058      //@ ensures (\result==TagConstants.CONDEXPR) ==> \typeof(this) <: \type(javafe.ast.CondExpr);
    059      //@ ensures (\result==TagConstants.INSTANCEOFEXPR) ==> \typeof(this) <: \type(javafe.ast.InstanceOfExpr);
    060      //@ ensures (\result==TagConstants.CASTEXPR) ==> \typeof(this) <: \type(javafe.ast.CastExpr);
    061      //@ ensures (\result==TagConstants.PARENEXPR) ==> \typeof(this) <: \type(javafe.ast.ParenExpr);
    062      //@ ensures (\result==TagConstants.AMBIGUOUSVARIABLEACCESS) ==> \typeof(this) <: \type(javafe.ast.AmbiguousVariableAccess);
    063      //@ ensures (\result==TagConstants.VARIABLEACCESS) ==> \typeof(this) <: \type(javafe.ast.VariableAccess);
    064      //@ ensures (\result==TagConstants.FIELDACCESS) ==> \typeof(this) <: \type(javafe.ast.FieldAccess);
    065      //@ ensures (\result==TagConstants.AMBIGUOUSMETHODINVOCATION) ==> \typeof(this) <: \type(javafe.ast.AmbiguousMethodInvocation);
    066      //@ ensures (\result==TagConstants.METHODINVOCATION) ==> \typeof(this) <: \type(javafe.ast.MethodInvocation);
    067      //@ ensures (\result==TagConstants.CLASSLITERAL) ==> \typeof(this) <: \type(javafe.ast.ClassLiteral);
    068      //@ ensures (\result==TagConstants.EXPROBJECTDESIGNATOR) ==> \typeof(this) <: \type(javafe.ast.ExprObjectDesignator);
    069      //@ ensures (\result==TagConstants.TYPEOBJECTDESIGNATOR) ==> \typeof(this) <: \type(javafe.ast.TypeObjectDesignator);
    070      //@ ensures (\result==TagConstants.SUPEROBJECTDESIGNATOR) ==> \typeof(this) <: \type(javafe.ast.SuperObjectDesignator);
    071      //@ ensures (\result==TagConstants.ERRORTYPE) ==> \typeof(this) <: \type(javafe.ast.ErrorType);
    072      //@ ensures (\result==TagConstants.TYPENAME) ==> \typeof(this) <: \type(javafe.ast.TypeName);
    073      //@ ensures (\result==TagConstants.ARRAYTYPE) ==> \typeof(this) <: \type(javafe.ast.ArrayType);
    074      //@ ensures (\result==TagConstants.SIMPLENAME) ==> \typeof(this) <: \type(javafe.ast.SimpleName);
    075      //@ ensures (\result==TagConstants.COMPOUNDNAME) ==> \typeof(this) <: \type(javafe.ast.CompoundName);
    076      //@ ensures (\result==TagConstants.OR) ==> \typeof(this) <: \type(javafe.ast.BinaryExpr);
    077      //@ ensures (\result==TagConstants.AND) ==> \typeof(this) <: \type(javafe.ast.BinaryExpr);
    078      //@ ensures (\result==TagConstants.BITOR) ==> \typeof(this) <: \type(javafe.ast.BinaryExpr);
    079      //@ ensures (\result==TagConstants.BITXOR) ==> \typeof(this) <: \type(javafe.ast.BinaryExpr);
    080      //@ ensures (\result==TagConstants.BITAND) ==> \typeof(this) <: \type(javafe.ast.BinaryExpr);
    081      //@ ensures (\result==TagConstants.NE) ==> \typeof(this) <: \type(javafe.ast.BinaryExpr);
    082      //@ ensures (\result==TagConstants.EQ) ==> \typeof(this) <: \type(javafe.ast.BinaryExpr);
    083      //@ ensures (\result==TagConstants.GE) ==> \typeof(this) <: \type(javafe.ast.BinaryExpr);
    084      //@ ensures (\result==TagConstants.GT) ==> \typeof(this) <: \type(javafe.ast.BinaryExpr);
    085      //@ ensures (\result==TagConstants.LE) ==> \typeof(this) <: \type(javafe.ast.BinaryExpr);
    086      //@ ensures (\result==TagConstants.LT) ==> \typeof(this) <: \type(javafe.ast.BinaryExpr);
    087      //@ ensures (\result==TagConstants.LSHIFT) ==> \typeof(this) <: \type(javafe.ast.BinaryExpr);
    088      //@ ensures (\result==TagConstants.RSHIFT) ==> \typeof(this) <: \type(javafe.ast.BinaryExpr);
    089      //@ ensures (\result==TagConstants.URSHIFT) ==> \typeof(this) <: \type(javafe.ast.BinaryExpr);
    090      //@ ensures (\result==TagConstants.ADD) ==> \typeof(this) <: \type(javafe.ast.BinaryExpr);
    091      //@ ensures (\result==TagConstants.SUB) ==> \typeof(this) <: \type(javafe.ast.BinaryExpr);
    092      //@ ensures (\result==TagConstants.DIV) ==> \typeof(this) <: \type(javafe.ast.BinaryExpr);
    093      //@ ensures (\result==TagConstants.MOD) ==> \typeof(this) <: \type(javafe.ast.BinaryExpr);
    094      //@ ensures (\result==TagConstants.STAR) ==> \typeof(this) <: \type(javafe.ast.BinaryExpr);
    095      //@ ensures (\result==TagConstants.ASSIGN) ==> \typeof(this) <: \type(javafe.ast.BinaryExpr);
    096      //@ ensures (\result==TagConstants.ASGMUL) ==> \typeof(this) <: \type(javafe.ast.BinaryExpr);
    097      //@ ensures (\result==TagConstants.ASGDIV) ==> \typeof(this) <: \type(javafe.ast.BinaryExpr);
    098      //@ ensures (\result==TagConstants.ASGREM) ==> \typeof(this) <: \type(javafe.ast.BinaryExpr);
    099      //@ ensures (\result==TagConstants.ASGADD) ==> \typeof(this) <: \type(javafe.ast.BinaryExpr);
    100      //@ ensures (\result==TagConstants.ASGSUB) ==> \typeof(this) <: \type(javafe.ast.BinaryExpr);
    101      //@ ensures (\result==TagConstants.ASGLSHIFT) ==> \typeof(this) <: \type(javafe.ast.BinaryExpr);
    102      //@ ensures (\result==TagConstants.ASGRSHIFT) ==> \typeof(this) <: \type(javafe.ast.BinaryExpr);
    103      //@ ensures (\result==TagConstants.ASGURSHIFT) ==> \typeof(this) <: \type(javafe.ast.BinaryExpr);
    104      //@ ensures (\result==TagConstants.ASGBITAND) ==> \typeof(this) <: \type(javafe.ast.BinaryExpr);
    105      //@ ensures (\result==TagConstants.ASGBITOR) ==> \typeof(this) <: \type(javafe.ast.BinaryExpr);
    106      //@ ensures (\result==TagConstants.ASGBITXOR) ==> \typeof(this) <: \type(javafe.ast.BinaryExpr);
    107      //@ ensures (\result==TagConstants.UNARYADD) ==> \typeof(this) <: \type(javafe.ast.UnaryExpr);
    108      //@ ensures (\result==TagConstants.UNARYSUB) ==> \typeof(this) <: \type(javafe.ast.UnaryExpr);
    109      //@ ensures (\result==TagConstants.NOT) ==> \typeof(this) <: \type(javafe.ast.UnaryExpr);
    110      //@ ensures (\result==TagConstants.BITNOT) ==> \typeof(this) <: \type(javafe.ast.UnaryExpr);
    111      //@ ensures (\result==TagConstants.INC) ==> \typeof(this) <: \type(javafe.ast.UnaryExpr);
    112      //@ ensures (\result==TagConstants.DEC) ==> \typeof(this) <: \type(javafe.ast.UnaryExpr);
    113      //@ ensures (\result==TagConstants.POSTFIXINC) ==> \typeof(this) <: \type(javafe.ast.UnaryExpr);
    114      //@ ensures (\result==TagConstants.POSTFIXDEC) ==> \typeof(this) <: \type(javafe.ast.UnaryExpr);
    115      //@ ensures (\result==TagConstants.BOOLEANTYPE) ==> \typeof(this) <: \type(javafe.ast.PrimitiveType);
    116      //@ ensures (\result==TagConstants.INTTYPE) ==> \typeof(this) <: \type(javafe.ast.PrimitiveType);
    117      //@ ensures (\result==TagConstants.LONGTYPE) ==> \typeof(this) <: \type(javafe.ast.PrimitiveType);
    118      //@ ensures (\result==TagConstants.CHARTYPE) ==> \typeof(this) <: \type(javafe.ast.PrimitiveType);
    119      //@ ensures (\result==TagConstants.FLOATTYPE) ==> \typeof(this) <: \type(javafe.ast.PrimitiveType);
    120      //@ ensures (\result==TagConstants.DOUBLETYPE) ==> \typeof(this) <: \type(javafe.ast.PrimitiveType);
    121      //@ ensures (\result==TagConstants.VOIDTYPE) ==> \typeof(this) <: \type(javafe.ast.PrimitiveType);
    122      //@ ensures (\result==TagConstants.NULLTYPE) ==> \typeof(this) <: \type(javafe.ast.PrimitiveType);
    123      //@ ensures (\result==TagConstants.BYTETYPE) ==> \typeof(this) <: \type(javafe.ast.PrimitiveType);
    124      //@ ensures (\result==TagConstants.SHORTTYPE) ==> \typeof(this) <: \type(javafe.ast.PrimitiveType);
    125      //@ ensures (\result==TagConstants.BOOLEANLIT) ==> \typeof(this) <: \type(javafe.ast.LiteralExpr);
    126      //@ ensures (\result==TagConstants.INTLIT) ==> \typeof(this) <: \type(javafe.ast.LiteralExpr);
    127      //@ ensures (\result==TagConstants.LONGLIT) ==> \typeof(this) <: \type(javafe.ast.LiteralExpr);
    128      //@ ensures (\result==TagConstants.CHARLIT) ==> \typeof(this) <: \type(javafe.ast.LiteralExpr);
    129      //@ ensures (\result==TagConstants.FLOATLIT) ==> \typeof(this) <: \type(javafe.ast.LiteralExpr);
    130      //@ ensures (\result==TagConstants.DOUBLELIT) ==> \typeof(this) <: \type(javafe.ast.LiteralExpr);
    131      //@ ensures (\result==TagConstants.STRINGLIT) ==> \typeof(this) <: \type(javafe.ast.LiteralExpr);
    132      //@ ensures (\result==TagConstants.NULLLIT) ==> \typeof(this) <: \type(javafe.ast.LiteralExpr);
    133        public int getTag();
    134
    135        public void accept(Visitor v);
    136
    137        public Object accept(VisitorArgResult v, Object o);
    138
    139        /**
    140         ** Do we have a parent field? <p>
    141         **
    142         ** A TypeDecl "invariant" requires all of its TypeDeclElem elements
    143         ** to have a parent. <p>
    144         **
    145         ** Known cases without parents:<p>
    146         **
    147         **   (a) non-member type TypeDecl's
    148         **   (b) TypeDeclElems before they are installed in a TypeDecl
    149         **   (c) The length FieldDecl  (belongs to no TypeDecl)
    150         **/
    151         //@ ghost public boolean hasParent;
    152
    153        /**
    154         ** The TypeDecl we are an element of, or null if we do not have a
    155         **  parent (cf. hasParent).
    156         **/
    157        //@ ensures hasParent ==> \result!=null;
    158        public TypeDecl getParent();
    159
    160        public void setParent(/*@non_null*/ TypeDecl p);
    161
    162        public int getModifiers();
    163        public void setModifiers(int m);
    164        public ModifierPragmaVec getPModifiers();
    165
    166        public int getStartLoc();
    167    }
    168