Overview | Package | Class | Use | Tree | Deprecated | Index | Help
| ESC/Java2 © 2003,2004,2005 David Cok and Joseph Kiniry © 2005 UCD Dublin © 2003,2004 Radboud University Nijmegen © 1999,2000 Compaq Computer Corporation © 1997,1998,1999 Digital Equipment Corporation All Rights Reserved
PREV CLASS NEXT CLASS | FRAMES NO FRAMES
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD

## escjava.ast
Class TagConstants

    java.lang.Object
      javafe.ast.GeneratedTags
          javafe.ast.OperatorTags
              javafe.ast.TagConstants
                  javafe.parser.TagConstants
                      javafe.tc.TagConstants
                          escjava.ast.GeneratedTags
                              escjava.ast.TagConstants

public class TagConstants
extends GeneratedTags

Field Summary
`static int` | `ABRUPT_BEHAVIOR`
`static int` | `ACCESSIBLE`
`static int` | `ACCESSIBLE_REDUNDANTLY`
`static int` | `ALLOCLE`
`static int` | `ALLOCLT`
`static int` | `ALSO`
`static int` | `ALSO_ENSURES`
`static int` | `ALSO_EXSURES`
`static int` | `ALSO_MODIFIES`
`static int` | `ALSO_REFINE`
`static int` | `ALSO_REQUIRES`
`static int` | `ANY`
`static int` | `ANYEQ`
`static int` | `ANYNE`
`static int` | `ARRAYFRESH`
`static int` | `ARRAYLENGTH`
`static int` | `ARRAYMAKE`
`static int` | `ARRAYSHAPEMORE`
`static int` | `ARRAYSHAPEONE`
`static int` | `ASELEMS`
`static int` | `ASFIELD`
`static int` | `ASLOCKSET`
`static int` | `ASSERT_REDUNDANTLY`
`static int` | `ASSERTCMD`
`static int` | `ASSIGNABLE`
`static int` | `ASSIGNABLE_REDUNDANTLY`
`static int` | `ASSUME`
`static int` | `ASSUME_REDUNDANTLY`
`static int` | `ASSUMECMD`
`static int` | `AXIOM`
`static int` | `BEHAVIOR`
`static int` | `BIGINT`
`static int` | `BIGINTTYPE`
`static int` | `BOOLAND`
`static int` | `BOOLANDX`
`static int` | `BOOLEQ`
`static int` | `BOOLIMPLIES`
`static int` | `BOOLNE`
`static int` | `BOOLNOT`
`static int` | `BOOLOR`
`static int` | `BREAKS`
`static int` | `BREAKS_REDUNDANTLY`
`static int` | `CALLABLE`
`static int` | `CALLABLE_REDUNDANTLY`
`static int` | `CAST`
`static int` | `CHK_AS_ASSERT`
`static int` | `CHK_AS_ASSUME`
`static int` | `CHK_AS_SKIP`
`static int` | `CHKADDINFO`
`static int` | `CHKARITHMETIC`
`static int` | `CHKARRAYSTORE`
`static int` | `CHKASSERT`
`static int` | `CHKASSUME`
`static int` | `CHKCLASSCAST`
`static int` | `CHKCODEREACHABILITY`
`static int` | `CHKCONSISTENT`
`static int` | `CHKCONSTRAINT`
`static int` | `CHKCONSTRUCTORLEAK`
`static int` | `CHKDECREASES_BOUND`
`static int` | `CHKDECREASES_DECR`
`static int` | `CHKDEFINEDNESS`
`static int` | `CHKFREE`
`static int` | `CHKINDEXNEGATIVE`
`static int` | `CHKINDEXTOOBIG`
`static int` | `CHKINITIALIZATION`
`static int` | `CHKINITIALIZERLEAK`
`static int` | `CHKINITIALLY`
`static int` | `CHKLOCKINGORDER`
`static int` | `CHKLOOPINVARIANT`
`static int` | `CHKLOOPOBJECTINVARIANT`
`static int` | `CHKMODIFIES`
`static int` | `CHKMODIFIESEXTENSION`
`static int` | `CHKNEGATIVEARRAYSIZE`
`static int` | `CHKNONNULL`
`static int` | `CHKNONNULLINIT`
`static int` | `CHKNONNULLRESULT`
`static int` | `CHKNULLPOINTER`
`static int` | `CHKOBJECTINVARIANT`
`static int` | `CHKOWNERNULL`
`static int` | `CHKPOSTCONDITION`
`static int` | `CHKPRECONDITION`
`static int` | `CHKQUIET`
`static int` | `CHKSHARING`
`static int` | `CHKSHARINGALLNULL`
`static int` | `CHKUNENFORCEBLEOBJECTINVARIANT`
`static int` | `CHKUNEXPECTEDEXCEPTION`
`static int` | `CHKUNEXPECTEDEXCEPTION2`
`static int` | `CHKWRITABLE`
`static int` | `CHKWRITABLEDEFERRED`
`static int` | `CHOOSE`
`static int` | `CHOOSE_IF`
`static int` | `CHOOSECMD`
`static int` | `CLASSLITERALFUNC`
`static int` | `CLOSEPRAGMA`
`static int` | `CODE_BIGINT_MATH`
`static int` | `CODE_CONTRACT`
`static int` | `CODE_JAVA_MATH`
`static int` | `CODE_SAFE_MATH`
`static int` | `CONDITIONAL`
`static int` | `CONSTRAINT`
`static int` | `CONSTRAINT_REDUNDANTLY`
`static int` | `CONSTRUCTOR`
`static int` | `CONTINUES`
`static int` | `CONTINUES_REDUNDANTLY`
`static int` | `DECREASES`
`static int` | `DECREASES_REDUNDANTLY`
`static int` | `DECREASING`
`static int` | `DECREASING_REDUNDANTLY`
`static int` | `DEPENDS`
`static int` | `DEPENDS_REDUNDANTLY`
`static int` | `DIVERGES`
`static int` | `DIVERGES_REDUNDANTLY`
`static int` | `DOTDOT`
`static int` | `DTTFSA`
`static int` | `DURATION`
`static int` | `DURATION_REDUNDANTLY`
`static int` | `ECLOSEDTIME`
`static int` | `ELEMSNONNULL`
`static int` | `ELEMTYPE`
`static int` | `END`
`static int` | `ENSURES`
`static int` | `ENSURES_REDUNDANTLY`
`static java.lang.String[]` | `escchecks`
`private static java.lang.String[]` | `escfunctions`
`private static Identifier[]` | `esckeywords`
`static int` | `EVERYTHING`
`static int` | `EXAMPLE`
`static int` | `EXCEPTIONAL_BEHAVIOR`
`static int` | `EXCEPTIONAL_EXAMPLE`
`static int` | `EXISTS`
`static int` | `EXPLIES`
`static int` | `EXSURES`
`static int` | `EXSURES_REDUNDANTLY`
`static Identifier` | `ExsuresIdnName`
`static int` | `FCLOSEDTIME`
`static int` | `FIELDKW`
`static int` | `FIELDS_OF`
`static int` | `FIRSTESCCHECKTAG`
`static int` | `FIRSTESCKEYWORDTAG`
`static int` | `FIRSTFUNCTIONTAG`
`static int` | `FIRSTJMLKEYWORDTAG`
`static int` | `FLOATINGADD`
`static int` | `FLOATINGDIV`
`static int` | `FLOATINGEQ`
`static int` | `FLOATINGGE`
`static int` | `FLOATINGGT`
`static int` | `FLOATINGLE`
`static int` | `FLOATINGLT`
`static int` | `FLOATINGMOD`
`static int` | `FLOATINGMUL`
`static int` | `FLOATINGNE`
`static int` | `FLOATINGNEG`
`static int` | `FLOATINGSUB`
`static int` | `FOR_EXAMPLE`
`static int` | `FORALL`
`static int` | `FRESH`
`static int` | `FUNCTION`
`static int` | `GHOST`
`static int` | `HELPER`
`static int` | `HENCE_BY`
`static int` | `HENCE_BY_REDUNDANTLY`
`static int` | `IFF`
`static int` | `IMMUTABLE`
`static int` | `IMPLIES`
`static int` | `IMPLIES_THAT`
`static int` | `IN`
`static int` | `IN_REDUNDANTLY`
`static int` | `INFORMALPRED_TOKEN`
`static int` | `INITIALIZER`
`static int` | `INITIALLY`
`static int` | `INSTANCE`
`static int` | `INTEGRALADD`
`static int` | `INTEGRALAND`
`static int` | `INTEGRALDIV`
`static int` | `INTEGRALEQ`
`static int` | `INTEGRALGE`
`static int` | `INTEGRALGT`
`static int` | `INTEGRALLE`
`static int` | `INTEGRALLT`
`static int` | `INTEGRALMOD`
`static int` | `INTEGRALMUL`
`static int` | `INTEGRALNE`
`static int` | `INTEGRALNEG`
`static int` | `INTEGRALNOT`
`static int` | `INTEGRALOR`
`static int` | `INTEGRALSUB`
`static int` | `INTEGRALXOR`
`static int` | `INTERN`
`static int` | `INTERNED`
`static int` | `INTO`
`static int` | `INTSHIFTL`
`static int` | `INTSHIFTR`
`static int` | `INTSHIFTRU`
`static int` | `INVARIANT`
`static int` | `INVARIANT_FOR`
`static int` | `INVARIANT_REDUNDANTLY`
`static int` | `IS`
`static int` | `IS_INITIALIZED`
`static int` | `ISALLOCATED`
`static int` | `ISNEWARRAY`
`private static Identifier[]` | `jmlkeywords`
`static int` | `LAST_TAG`
`static int` | `LASTESCCHECKTAG`
`static int` | `LASTESCKEYWORDTAG`
`static int` | `LASTFUNCTIONTAG`
`static int` | `LASTJMLKEYWORDTAG`
`static int` | `LBLNEG`
`static int` | `LBLPOS`
`static int` | `LEFTARROW`
`static int` | `LOCKLE`
`static int` | `LOCKLT`
`static int` | `LOCKSET`
`static int` | `LONGSHIFTL`
`static int` | `LONGSHIFTR`
`static int` | `LONGSHIFTRU`
`static int` | `LOOP_INVARIANT`
`static int` | `LOOP_INVARIANT_REDUNDANTLY`
`static int` | `LOOP_PREDICATE`
`static int` | `LS`
`static int` | `MAINTAINING`
`static int` | `MAINTAINING_REDUNDANTLY`
`static int` | `MAPS`
`static int` | `MAPS_REDUNDANTLY`
`static int` | `MAX`
`static int` | `MAXQUANT`
`static int` | `MAY_BE_NULL`
`static int` | `MEASURED_BY`
`static int` | `MEASURED_BY_REDUNDANTLY`
`static int` | `METHOD`
`static int` | `METHODCALL`
`static int` | `MIN`
`static int` | `MODEL`
`static int` | `MODEL_PROGRAM`
`static int` | `MODELPROGRAM_OR`
`static int` | `MODIFIABLE`
`static int` | `MODIFIABLE_REDUNDANTLY`
`static int` | `MODIFIES`
`static int` | `MODIFIES_REDUNDANTLY`
`static int` | `MONITORED`
`static int` | `MONITORED_BY`
`static int` | `MONITORS_FOR`
`static int` | `NESTEDMODIFIERPRAGMA`
`static int` | `NIFF`
`static int` | `NO_WACK_FORALL`
`static int` | `NON_NULL`
`static int` | `NON_NULL_REF_BY_DEFAULT`
`static int` | `NORMAL_BEHAVIOR`
`static int` | `NORMAL_EXAMPLE`
`static int` | `NOT_MODIFIED`
`static int` | `NOT_SPECIFIED`
`static int` | `NOTHING`
`static int` | `NOWARN`
`static int` | `NOWARN_OP`
`static int` | `NULL_REF_BY_DEFAULT`
`static int` | `NUM_OF`
`static int` | `OBJECTSET`
`static int` | `OBS_PURE`
`static int` | `OLD`
`static int` | `OPENPRAGMA`
`static int` | `OTHER`
`static int` | `PARSEDSPECS`
`static int` | `PEER`
`static int` | `POSTCONDITION`
`static int` | `POSTCONDITION_REDUNDANTLY`
`static int` | `PRE`
`static int` | `PRECONDITION`
`static int` | `PRECONDITION_REDUNDANTLY`
`static int` | `PRIVATE_DATA`
`static int` | `PRODUCT`
`static int` | `PURE`
`static int` | `RAISECMD`
`static int` | `REACH`
`static int` | `READABLE`
`static int` | `READABLE_IF`
`static int` | `READONLY`
`static int` | `REAL`
`static int` | `REALTYPE`
`static int` | `REFEQ`
`static int` | `REFINE`
`static int` | `REFNE`
`static int` | `REP`
`static int` | `REPRESENTS`
`static int` | `REPRESENTS_REDUNDANTLY`
`static int` | `REQUIRES`
`static int` | `REQUIRES_REDUNDANTLY`
`static int` | `RES`
`static int` | `RETURNS`
`static int` | `RETURNS_REDUNDANTLY`
`static int` | `RIGHTARROW`
`static int` | `SELECT`
`static int` | `SET`
`static int` | `SIGNALS`
`static int` | `SIGNALS_ONLY`
`static int` | `SIGNALS_REDUNDANTLY`
`static int` | `SKIPCMD`
`static int` | `SKOLEM_CONSTANT`
`static int` | `SPACE`
`static int` | `SPEC_BIGINT_MATH`
`static int` | `SPEC_JAVA_MATH`
`static int` | `SPEC_PROTECTED`
`static int` | `SPEC_PUBLIC`
`static int` | `SPEC_SAFE_MATH`
`static int` | `STATIC_INITIALIZER`
`static int` | `STILL_DEFERRED`
`static int` | `STORE`
`static int` | `STRINGCAT`
`static java.lang.String` | `STRINGCATINFIX`
`static int` | `STRINGCATP`
`static int` | `SUBCLASSING_CONTRACT`
`static int` | `SUBTYPE`
`static int` | `SUCH_THAT`
`static int` | `SUM`
`static int` | `SYMBOLLIT`
`static int` | `TRYCMD`
`static int` | `TYPE`
`static int` | `TYPECODE`
`static int` | `TYPEEQ`
`static int` | `TYPELE`
`static int` | `TYPENE`
`static int` | `TYPEOF`
`static int` | `TYPETYPE`
`static int` | `UNINITIALIZED`
`static int` | `UNREACHABLE`
`static int` | `UNSET`
`static int` | `VALLOCTIME`
`static int` | `WACK_BIGINT_MATH`
`static int` | `WACK_DURATION`
`static int` | `WACK_JAVA_MATH`
`static int` | `WACK_NOWARN`
`static int` | `WACK_SAFE_MATH`
`static int` | `WACK_WORKING_SPACE`
`static int` | `WARN`
`static int` | `WARN_OP`
`static int` | `WEAKLY`
`static int` | `WHEN`
`static int` | `WHEN_REDUNDANTLY`
`static int` | `WORKING_SPACE`
`static int` | `WORKING_SPACE_REDUNDANTLY`
`static int` | `WRITABLE`
`static int` | `WRITABLE_DEFERRED`
`static int` | `WRITABLE_IF`

Fields inherited from class escjava.ast.GeneratedTags
`ARRAYRANGEREFEXPR, CALL, CONDITION, DEFPRED, DEFPREDAPPLEXPR, DEFPREDLETEXPR, DYNINSTCMD, EVERYTHINGEXPR, GETSCMD, GHOSTDECLPRAGMA, GUARDEXPR, IDENTIFIERMODIFIERPRAGMA, IMPORTPRAGMA, LABELEXPR, LOCKSETEXPR, LOOPCMD, MODELCONSTRUCTORDECLPRAGMA, MODELDECLPRAGMA, MODELMETHODDECLPRAGMA, MODELTYPEPRAGMA, MODIFIESGROUPPRAGMA, NOTHINGEXPR, NOTMODIFIEDEXPR, NOTSPECIFIEDEXPR, NOWARNPRAGMA, REACHMODIFIERPRAGMA, REFINEPRAGMA, RESEXPR, RESTOREFROMCMD, SEQCMD, SETCOMPEXPR, SETSTMTPRAGMA, SKOLEMCONSTANTPRAGMA, SPEC, STILLDEFERREDDECLPRAGMA, SUBGETSCMD, SUBSTEXPR, SUBSUBGETSCMD, TYPEEXPR, VARINCMD, WILDREFEXPR`

Fields inherited from class javafe.tc.TagConstants
`TYPESIG`

Fields inherited from class javafe.parser.TagConstants
`ABSTRACT, ASSERT, BOOLEAN, BREAK, BYTE, C_COMMENT, CASE, CATCH, CHAR, CLASS, COLON, COMMA, CONST, CONTINUE, DEFAULT, DO, DOUBLE, ELSE, EOF, EOL_COMMENT, EXTENDS, FALSE, FIELD, FINAL, FINALLY, FIRST_KEYWORD, FLOAT, FOR, GOTO, IF, IMPLEMENTS, IMPORT, INSTANCEOF, INT, INTERFACE, LAST_KEYWORD, LBRACE, LEXICALPRAGMA, LONG, LPAREN, LSQBRACKET, MAX_INT_PLUS_ONE, MAX_LONG_PLUS_ONE, MODIFIERPRAGMA, NATIVE, NEW, NULL, PACKAGE, POSTMODIFIERPRAGMA, PRIVATE, PROTECTED, PUBLIC, QUESTIONMARK, RBRACE, RETURN, RPAREN, RSQBRACKET, SEMICOLON, SHORT, STATIC, STMTPRAGMA, STRICT, SUPER, SWITCH, SYNCHRONIZED, THIS, THROW, THROWS, TRANSIENT, TRUE, TRY, TYPEDECLELEMPRAGMA, TYPEMODIFIERPRAGMA, UNKNOWN_KEYWORD, VOID, VOLATILE, WHILE`

Fields inherited from class javafe.ast.TagConstants
`BOOLEANLIT, BOOLEANTYPE, BYTELIT, BYTETYPE, CHARLIT, CHARTYPE, DOUBLELIT, DOUBLETYPE, ERRORTYPE, FLOATLIT, FLOATTYPE, IDENT, INTLIT, INTTYPE, LONGLIT, LONGTYPE, NULLLIT, NULLTYPE, SHORTLIT, SHORTTYPE, STRINGLIT, VOIDTYPE`

Fields inherited from class javafe.ast.OperatorTags
`ADD, AND, ASGADD, ASGBITAND, ASGBITOR, ASGBITXOR, ASGDIV, ASGLSHIFT, ASGMUL, ASGREM, ASGRSHIFT, ASGSUB, ASGURSHIFT, ASSIGN, BITAND, BITNOT, BITOR, BITXOR, DEC, DIV, EQ, FIRST_TAG, GE, GT, INC, LE, LSHIFT, LT, MOD, NE, NOT, OR, POSTFIXDEC, POSTFIXINC, RSHIFT, STAR, SUB, UNARYADD, UNARYSUB, URSHIFT`

Fields inherited from class javafe.ast.GeneratedTags
`AMBIGUOUSMETHODINVOCATION, AMBIGUOUSVARIABLEACCESS, ARRAYINIT, ARRAYREFEXPR, ARRAYTYPE, ASSERTSTMT, BLOCKSTMT, BREAKSTMT, CASTEXPR, CATCHCLAUSE, CLASSDECL, CLASSDECLSTMT, CLASSLITERAL, COMPILATIONUNIT, COMPOUNDNAME, CONDEXPR, CONSTRUCTORDECL, CONSTRUCTORINVOCATION, CONTINUESTMT, DOSTMT, EVALSTMT, EXPROBJECTDESIGNATOR, FIELDACCESS, FIELDDECL, FORMALPARADECL, FORSTMT, IFSTMT, INITBLOCK, INSTANCEOFEXPR, INTERFACEDECL, LABELSTMT, LOCALVARDECL, METHODDECL, METHODINVOCATION, NEWARRAYEXPR, NEWINSTANCEEXPR, ONDEMANDIMPORTDECL, PARENEXPR, RETURNSTMT, SIMPLENAME, SINGLETYPEIMPORTDECL, SKIPSTMT, SUPEROBJECTDESIGNATOR, SWITCHLABEL, SWITCHSTMT, SYNCHRONIZESTMT, THISEXPR, THROWSTMT, TRYCATCHSTMT, TRYFINALLYSTMT, TYPENAME, TYPEOBJECTDESIGNATOR, VARDECLSTMT, VARIABLEACCESS, WHILESTMT`

Constructor Summary
`TagConstants()`

Method Summary
`static int` | `checkFromString(java.lang.String s)`
`private static void` | `comp(int i, int j, java.lang.String s)`
`static int` | `fromIdentifier(Identifier keyword)`
`static boolean` | `isKeywordTag(int tag)`
`static boolean` | `isRedundant(int tag)`
`static void` | `main(java.lang.String[] args)`
`static int` | `makeRedundant(int tag)`
`static java.lang.String` | `toString(int tag)`
`static java.lang.String` | `toVcString(int tag)`
`static int` | `unRedundant(int tag)`

Methods inherited from class javafe.parser.TagConstants
`zzzz`

Methods inherited from class java.lang.Object
`clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait`

Field Detail

### IMPLIES

    public static final int IMPLIES

See Also:
  Constant Field Values

### EXPLIES

    public static final int EXPLIES

See Also:
  Constant Field Values

### IFF

    public static final int IFF

See Also:
  Constant Field Values

### NIFF

    public static final int NIFF

See Also:
  Constant Field Values

### SUBTYPE

    public static final int SUBTYPE

See Also:
  Constant Field Values

### DOTDOT

    public static final int DOTDOT

See Also:
  Constant Field Values

### LEFTARROW

    public static final int LEFTARROW

See Also:
  Constant Field Values

### RIGHTARROW

    public static final int RIGHTARROW

See Also:
  Constant Field Values

### OPENPRAGMA

    public static final int OPENPRAGMA

See Also:
  Constant Field Values

### CLOSEPRAGMA

    public static final int CLOSEPRAGMA

See Also:
  Constant Field Values

### SYMBOLLIT

    public static final int SYMBOLLIT

See Also:
  Constant Field Values

### ANY

    public static final int ANY

See Also:
  Constant Field Values

### TYPECODE

    public static final int TYPECODE

See Also:
  Constant Field Values

### BIGINTTYPE

    public static final int BIGINTTYPE

See Also:
  Constant Field Values

### REALTYPE

    public static final int REALTYPE

See Also:
  Constant Field Values

### LOCKSET

    public static final int LOCKSET

See Also:
  Constant Field Values

### OBJECTSET

    public static final int OBJECTSET

See Also:
  Constant Field Values

### ASSERTCMD

    public static final int ASSERTCMD

See Also:
  Constant Field Values

### ASSUMECMD

    public static final int ASSUMECMD

See Also:
  Constant Field Values

### CHOOSECMD

    public static final int CHOOSECMD

See Also:
  Constant Field Values

### RAISECMD

    public static final int RAISECMD

See Also:
  Constant Field Values

### SKIPCMD

    public static final int SKIPCMD

See Also:
  Constant Field Values

### TRYCMD

    public static final int TRYCMD

See Also:
  Constant Field Values

### INFORMALPRED_TOKEN

    public static final int INFORMALPRED_TOKEN

See Also:
  Constant Field Values

### FIRSTESCCHECKTAG

    public static final int FIRSTESCCHECKTAG

See Also:
  Constant Field Values

### CHKARITHMETIC

    public static final int CHKARITHMETIC

See Also:
  Constant Field Values

### CHKARRAYSTORE

    public static final int CHKARRAYSTORE

See Also:
  Constant Field Values

### CHKASSERT

    public static final int CHKASSERT

See Also:
  Constant Field Values

### CHKCLASSCAST

    public static final int CHKCLASSCAST

See Also:
  Constant Field Values

### CHKCODEREACHABILITY

    public static final int CHKCODEREACHABILITY

See Also:
  Constant Field Values

### CHKCONSISTENT

    public static final int CHKCONSISTENT

See Also:
  Constant Field Values

### CHKCONSTRAINT

    public static final int CHKCONSTRAINT

See Also:
  Constant Field Values

### CHKCONSTRUCTORLEAK

    public static final int CHKCONSTRUCTORLEAK

See Also:
  Constant Field Values

### CHKDECREASES_BOUND

    public static final int CHKDECREASES_BOUND

See Also:
  Constant Field Values

### CHKDECREASES_DECR

    public static final int CHKDECREASES_DECR

See Also:
  Constant Field Values

### CHKDEFINEDNESS

    public static final int CHKDEFINEDNESS

See Also:
  Constant Field Values

### CHKINDEXNEGATIVE

    public static final int CHKINDEXNEGATIVE

See Also:
  Constant Field Values

### CHKINDEXTOOBIG

    public static final int CHKINDEXTOOBIG

See Also:
  Constant Field Values

### CHKINITIALIZATION

    public static final int CHKINITIALIZATION

See Also:
  Constant Field Values

### CHKINITIALIZERLEAK

    public static final int CHKINITIALIZERLEAK

See Also:
  Constant Field Values

### CHKINITIALLY

    public static final int CHKINITIALLY

See Also:
  Constant Field Values

### CHKLOCKINGORDER

    public static final int CHKLOCKINGORDER

See Also:
  Constant Field Values

### CHKLOOPINVARIANT

    public static final int CHKLOOPINVARIANT

See Also:
  Constant Field Values

### CHKLOOPOBJECTINVARIANT

    public static final int CHKLOOPOBJECTINVARIANT

See Also:
  Constant Field Values

### CHKMODIFIESEXTENSION

    public static final int CHKMODIFIESEXTENSION

See Also:
  Constant Field Values

### CHKMODIFIES

    public static final int CHKMODIFIES

See Also:
  Constant Field Values

### CHKNEGATIVEARRAYSIZE

    public static final int CHKNEGATIVEARRAYSIZE

See Also:
  Constant Field Values

### CHKNONNULL

    public static final int CHKNONNULL

See Also:
  Constant Field Values

### CHKNONNULLINIT

    public static final int CHKNONNULLINIT

See Also:
  Constant Field Values

### CHKNONNULLRESULT

    public static final int CHKNONNULLRESULT

See Also:
  Constant Field Values

### CHKNULLPOINTER

    public static final int CHKNULLPOINTER

See Also:
  Constant Field Values

### CHKOBJECTINVARIANT

    public static final int CHKOBJECTINVARIANT

See Also:
  Constant Field Values

### CHKOWNERNULL

    public static final int CHKOWNERNULL

See Also:
  Constant Field Values

### CHKPOSTCONDITION

    public static final int CHKPOSTCONDITION

See Also:
  Constant Field Values

### CHKPRECONDITION

    public static final int CHKPRECONDITION

See Also:
  Constant Field Values

### CHKSHARING

    public static final int CHKSHARING

See Also:
  Constant Field Values

### CHKSHARINGALLNULL

    public static final int CHKSHARINGALLNULL

See Also:
  Constant Field Values

### CHKUNENFORCEBLEOBJECTINVARIANT

    public static final int CHKUNENFORCEBLEOBJECTINVARIANT

See Also:
  Constant Field Values

### CHKUNEXPECTEDEXCEPTION

    public static final int CHKUNEXPECTEDEXCEPTION

See Also:
  Constant Field Values

### CHKUNEXPECTEDEXCEPTION2

    public static final int CHKUNEXPECTEDEXCEPTION2

See Also:
  Constant Field Values

### CHKWRITABLEDEFERRED

    public static final int CHKWRITABLEDEFERRED

See Also:
  Constant Field Values

### CHKWRITABLE

    public static final int CHKWRITABLE

See Also:
  Constant Field Values

### CHKQUIET

    public static final int CHKQUIET

See Also:
  Constant Field Values

### CHKASSUME

    public static final int CHKASSUME

See Also:
  Constant Field Values

### CHKADDINFO

    public static final int CHKADDINFO

See Also:
  Constant Field Values

### CHKFREE

    public static final int CHKFREE

See Also:
  Constant Field Values

### LASTESCCHECKTAG

    public static final int LASTESCCHECKTAG

See Also:
  Constant Field Values

### FIRSTFUNCTIONTAG

    public static final int FIRSTFUNCTIONTAG

See Also:
  Constant Field Values

### ALLOCLT

    public static final int ALLOCLT

See Also:
  Constant Field Values

### ALLOCLE

    public static final int ALLOCLE

See Also:
  Constant Field Values

### ANYEQ

    public static final int ANYEQ

See Also:
  Constant Field Values

### ANYNE

    public static final int ANYNE

See Also:
  Constant Field Values

### ARRAYLENGTH

    public static final int ARRAYLENGTH

See Also:
  Constant Field Values

### ARRAYFRESH

    public static final int ARRAYFRESH

See Also:
  Constant Field Values

### ARRAYMAKE

    public static final int ARRAYMAKE

See Also:
  Constant Field Values

### ARRAYSHAPEMORE

    public static final int ARRAYSHAPEMORE

See Also:
  Constant Field Values

### ARRAYSHAPEONE

    public static final int ARRAYSHAPEONE

See Also:
  Constant Field Values

### ASELEMS

    public static final int ASELEMS

See Also:
  Constant Field Values

### ASFIELD

    public static final int ASFIELD

See Also:
  Constant Field Values

### ASLOCKSET

    public static final int ASLOCKSET

See Also:
  Constant Field Values

### BOOLAND

    public static final int BOOLAND

See Also:
  Constant Field Values

### BOOLANDX

    public static final int BOOLANDX

See Also:
  Constant Field Values

### BOOLEQ

    public static final int BOOLEQ

See Also:
  Constant Field Values

### BOOLIMPLIES

    public static final int BOOLIMPLIES

See Also:
  Constant Field Values

### BOOLNE

    public static final int BOOLNE

See Also:
  Constant Field Values

### BOOLNOT

    public static final int BOOLNOT

See Also:
  Constant Field Values

### BOOLOR

    public static final int BOOLOR

See Also:
  Constant Field Values

### CAST

    public static final int CAST

See Also:
  Constant Field Values

### CLASSLITERALFUNC

    public static final int CLASSLITERALFUNC

See Also:
  Constant Field Values

### CONDITIONAL

    public static final int CONDITIONAL

See Also:
  Constant Field Values

### ECLOSEDTIME

    public static final int ECLOSEDTIME

See Also:
  Constant Field Values

### FCLOSEDTIME

    public static final int FCLOSEDTIME

See Also:
  Constant Field Values

### FLOATINGADD

    public static final int FLOATINGADD

See Also:
  Constant Field Values

### FLOATINGDIV

    public static final int FLOATINGDIV

See Also:
  Constant Field Values

### FLOATINGEQ

    public static final int FLOATINGEQ

See Also:
  Constant Field Values

### FLOATINGGE

    public static final int FLOATINGGE

See Also:
  Constant Field Values

### FLOATINGGT

    public static final int FLOATINGGT

See Also:
  Constant Field Values

### FLOATINGLE

    public static final int FLOATINGLE

See Also:
  Constant Field Values

### FLOATINGLT

    public static final int FLOATINGLT

See Also:
  Constant Field Values

### FLOATINGMOD

    public static final int FLOATINGMOD

See Also:
  Constant Field Values

### FLOATINGMUL

    public static final int FLOATINGMUL

See Also:
  Constant Field Values

### FLOATINGNE

    public static final int FLOATINGNE

See Also:
  Constant Field Values

### FLOATINGNEG

    public static final int FLOATINGNEG

See Also:
  Constant Field Values

### FLOATINGSUB

    public static final int FLOATINGSUB

See Also:
  Constant Field Values

### INTEGRALADD

    public static final int INTEGRALADD

See Also:
  Constant Field Values

### INTEGRALAND

    public static final int INTEGRALAND

See Also:
  Constant Field Values

### INTEGRALDIV

    public static final int INTEGRALDIV

See Also:
  Constant Field Values

### INTEGRALEQ

    public static final int INTEGRALEQ

See Also:
  Constant Field Values

### INTEGRALGE

    public static final int INTEGRALGE

See Also:
  Constant Field Values

### INTEGRALGT

    public static final int INTEGRALGT

See Also:
  Constant Field Values

### INTEGRALLE

    public static final int INTEGRALLE

See Also:
  Constant Field Values

### INTEGRALLT

    public static final int INTEGRALLT

See Also:
  Constant Field Values

### INTEGRALMOD

    public static final int INTEGRALMOD

See Also:
  Constant Field Values

### INTEGRALMUL

    public static final int INTEGRALMUL

See Also:
  Constant Field Values

### INTEGRALNE

    public static final int INTEGRALNE

See Also:
  Constant Field Values

### INTEGRALNEG

    public static final int INTEGRALNEG

See Also:
  Constant Field Values

### INTEGRALNOT

    public static final int INTEGRALNOT

See Also:
  Constant Field Values

### INTEGRALOR

    public static final int INTEGRALOR

See Also:
  Constant Field Values

### INTSHIFTL

    public static final int INTSHIFTL

See Also:
  Constant Field Values

### LONGSHIFTL

    public static final int LONGSHIFTL

See Also:
  Constant Field Values

### INTSHIFTR

    public static final int INTSHIFTR

See Also:
  Constant Field Values

### LONGSHIFTR

    public static final int LONGSHIFTR

See Also:
  Constant Field Values

### INTSHIFTRU

    public static final int INTSHIFTRU

See Also:
  Constant Field Values

### LONGSHIFTRU

    public static final int LONGSHIFTRU

See Also:
  Constant Field Values

### INTEGRALSUB

    public static final int INTEGRALSUB

See Also:
  Constant Field Values

### INTEGRALXOR

    public static final int INTEGRALXOR

See Also:
  Constant Field Values

### INTERN

    public static final int INTERN

See Also:
  Constant Field Values

### INTERNED

    public static final int INTERNED

See Also:
  Constant Field Values

### IS

    public static final int IS

See Also:
  Constant Field Values

### ISALLOCATED

    public static final int ISALLOCATED

See Also:
  Constant Field Values

### ISNEWARRAY

    public static final int ISNEWARRAY

See Also:
  Constant Field Values

### LOCKLE

    public static final int LOCKLE

See Also:
  Constant Field Values

### LOCKLT

    public static final int LOCKLT

See Also:
  Constant Field Values

### METHODCALL

    public static final int METHODCALL

See Also:
  Constant Field Values

### REFEQ

    public static final int REFEQ

See Also:
  Constant Field Values

### REFNE

    public static final int REFNE

See Also:
  Constant Field Values

### SELECT

    public static final int SELECT

See Also:
  Constant Field Values

### STORE

    public static final int STORE

See Also:
  Constant Field Values

### STRINGCAT

    public static final int STRINGCAT

See Also:
  Constant Field Values

### STRINGCATP

    public static final int STRINGCATP

See Also:
  Constant Field Values

### TYPEEQ

    public static final int TYPEEQ

See Also:
  Constant Field Values

### TYPENE

    public static final int TYPENE

See Also:
  Constant Field Values

### TYPELE

    public static final int TYPELE

See Also:
  Constant Field Values

### UNSET

    public static final int UNSET

See Also:
  Constant Field Values

### VALLOCTIME

    public static final int VALLOCTIME

See Also:
  Constant Field Values

### LASTFUNCTIONTAG

    public static final int LASTFUNCTIONTAG

See Also:
  Constant Field Values

### CHK_AS_ASSUME

    public static final int CHK_AS_ASSUME

See Also:
  Constant Field Values

### CHK_AS_ASSERT

    public static final int CHK_AS_ASSERT

See Also:
  Constant Field Values

### CHK_AS_SKIP

    public static final int CHK_AS_SKIP

See Also:
  Constant Field Values

### FIRSTJMLKEYWORDTAG

    public static final int FIRSTJMLKEYWORDTAG

See Also:
  Constant Field Values

### ASSUME

    public static final int ASSUME

See Also:
  Constant Field Values

### AXIOM

    public static final int AXIOM

See Also:
  Constant Field Values

### CODE_CONTRACT

    public static final int CODE_CONTRACT

See Also:
  Constant Field Values

### DECREASES

    public static final int DECREASES

See Also:
  Constant Field Values

### DTTFSA

    public static final int DTTFSA

See Also:
  Constant Field Values

### ENSURES

    public static final int ENSURES

See Also:
  Constant Field Values

### ELEMSNONNULL

    public static final int ELEMSNONNULL

See Also:
  Constant Field Values

### ELEMTYPE

    public static final int ELEMTYPE

See Also:
  Constant Field Values

### EXISTS

    public static final int EXISTS

See Also:
  Constant Field Values

### EXSURES

    public static final int EXSURES

See Also:
  Constant Field Values

### FRESH

    public static final int FRESH

See Also:
  Constant Field Values

### FORALL

    public static final int FORALL

See Also:
  Constant Field Values

### FUNCTION

    public static final int FUNCTION

See Also:
  Constant Field Values

### GHOST

    public static final int GHOST

See Also:
  Constant Field Values

### HELPER

    public static final int HELPER

See Also:
  Constant Field Values

### IMMUTABLE

    public static final int IMMUTABLE

See Also:
  Constant Field Values

### IN

    public static final int IN

See Also:
  Constant Field Values

### IN_REDUNDANTLY

    public static final int IN_REDUNDANTLY

See Also:
  Constant Field Values

### INTO

    public static final int INTO

See Also:
  Constant Field Values

### INVARIANT

    public static final int INVARIANT

See Also:
  Constant Field Values

### LBLPOS

    public static final int LBLPOS

See Also:
  Constant Field Values

### LBLNEG

    public static final int LBLNEG

See Also:
  Constant Field Values

### LOOP_INVARIANT

    public static final int LOOP_INVARIANT

See Also:
  Constant Field Values

### LOOP_PREDICATE

    public static final int LOOP_PREDICATE

See Also:
  Constant Field Values

### LS

    public static final int LS

See Also:
  Constant Field Values

### MAPS

    public static final int MAPS

See Also:
  Constant Field Values

### MAPS_REDUNDANTLY

    public static final int MAPS_REDUNDANTLY

See Also:
  Constant Field Values

### MAX

    public static final int MAX

See Also:
  Constant Field Values

### MODIFIES

    public static final int MODIFIES

See Also:
  Constant Field Values

### MONITORED

    public static final int MONITORED

See Also:
  Constant Field Values

### MONITORED_BY

    public static final int MONITORED_BY

See Also:
  Constant Field Values

### MONITORS_FOR

    public static final int MONITORS_FOR

See Also:
  Constant Field Values

### NON_NULL

    public static final int NON_NULL

See Also:
  Constant Field Values

### NOWARN

    public static final int NOWARN

See Also:
  Constant Field Values

### PRE

    public static final int PRE

See Also:
  Constant Field Values

### READABLE

    public static final int READABLE

See Also:
  Constant Field Values

### READABLE_IF

    public static final int READABLE_IF

See Also:
  Constant Field Values

### RES

    public static final int RES

See Also:
  Constant Field Values

### REQUIRES

    public static final int REQUIRES

See Also:
  Constant Field Values

### SET

    public static final int SET

See Also:
  Constant Field Values

### SPEC_PUBLIC

    public static final int SPEC_PUBLIC

See Also:
  Constant Field Values

### STILL_DEFERRED

    public static final int STILL_DEFERRED

See Also:
  Constant Field Values

### TYPE

    public static final int TYPE

See Also:
  Constant Field Values

### TYPETYPE

    public static final int TYPETYPE

See Also:
  Constant Field Values

### TYPEOF

    public static final int TYPEOF

See Also:
  Constant Field Values

### UNINITIALIZED

    public static final int UNINITIALIZED

See Also:
  Constant Field Values

### UNREACHABLE

    public static final int UNREACHABLE

See Also:
  Constant Field Values

### WRITABLE_DEFERRED

    public static final int WRITABLE_DEFERRED

See Also:
  Constant Field Values

### WRITABLE_IF

    public static final int WRITABLE_IF

See Also:
  Constant Field Values

### WRITABLE

    public static final int WRITABLE

See Also:
  Constant Field Values

### SKOLEM_CONSTANT

    public static final int SKOLEM_CONSTANT

See Also:
  Constant Field Values

### BIGINT

    public static final int BIGINT

See Also:
  Constant Field Values

### WACK_DURATION

    public static final int WACK_DURATION

See Also:
  Constant Field Values

### EVERYTHING

    public static final int EVERYTHING

See Also:
  Constant Field Values

### FIELDS_OF

    public static final int FIELDS_OF

See Also:
  Constant Field Values

### INVARIANT_FOR

    public static final int INVARIANT_FOR

See Also:
  Constant Field Values

### IS_INITIALIZED

    public static final int IS_INITIALIZED

See Also:
  Constant Field Values

### MAXQUANT

    public static final int MAXQUANT

See Also:
  Constant Field Values

### MIN

    public static final int MIN

See Also:
  Constant Field Values

### NOTHING

    public static final int NOTHING

See Also:
  Constant Field Values

### NOT_MODIFIED

    public static final int NOT_MODIFIED

See Also:
  Constant Field Values

### NOT_SPECIFIED

    public static final int NOT_SPECIFIED

See Also:
  Constant Field Values

### WACK_NOWARN

    public static final int WACK_NOWARN

See Also:
  Constant Field Values

### NOWARN_OP

    public static final int NOWARN_OP

See Also:
  Constant Field Values

### NUM_OF

    public static final int NUM_OF

See Also:
  Constant Field Values

### OTHER

    public static final int OTHER

See Also:
  Constant Field Values

### PRIVATE_DATA

    public static final int PRIVATE_DATA

See Also:
  Constant Field Values

### PRODUCT

    public static final int PRODUCT

See Also:
  Constant Field Values

### REACH

    public static final int REACH

See Also:
  Constant Field Values

### REAL

    public static final int REAL

See Also:
  Constant Field Values

### SPACE

    public static final int SPACE

See Also:
  Constant Field Values

### SUCH_THAT

    public static final int SUCH_THAT

See Also:
  Constant Field Values

### SUM

    public static final int SUM

See Also:
  Constant Field Values

### WARN

    public static final int WARN

See Also:
  Constant Field Values

### WARN_OP

    public static final int WARN_OP

See Also:
  Constant Field Values

### WACK_WORKING_SPACE

    public static final int WACK_WORKING_SPACE

See Also:
  Constant Field Values

### ABRUPT_BEHAVIOR

    public static final int ABRUPT_BEHAVIOR

See Also:
  Constant Field Values

### ACCESSIBLE_REDUNDANTLY

    public static final int ACCESSIBLE_REDUNDANTLY

See Also:
  Constant Field Values

### ACCESSIBLE

    public static final int ACCESSIBLE

See Also:
  Constant Field Values

### ALSO

    public static final int ALSO

See Also:
  Constant Field Values

### ALSO_REFINE

    public static final int ALSO_REFINE

See Also:
  Constant Field Values

### ASSERT_REDUNDANTLY

    public static final int ASSERT_REDUNDANTLY

See Also:
  Constant Field Values

### ASSIGNABLE_REDUNDANTLY

    public static final int ASSIGNABLE_REDUNDANTLY

See Also:
  Constant Field Values

### ASSIGNABLE

    public static final int ASSIGNABLE

See Also:
  Constant Field Values

### ASSUME_REDUNDANTLY

    public static final int ASSUME_REDUNDANTLY

See Also:
  Constant Field Values

### BEHAVIOR

    public static final int BEHAVIOR

See Also:
  Constant Field Values

### BREAKS_REDUNDANTLY

    public static final int BREAKS_REDUNDANTLY

See Also:
  Constant Field Values

### BREAKS

    public static final int BREAKS

See Also:
  Constant Field Values

### CALLABLE_REDUNDANTLY

    public static final int CALLABLE_REDUNDANTLY

See Also:
  Constant Field Values

### CALLABLE

    public static final int CALLABLE

See Also:
  Constant Field Values

### CHOOSE_IF

    public static final int CHOOSE_IF

See Also:
  Constant Field Values

### CHOOSE

    public static final int CHOOSE

See Also:
  Constant Field Values

### CONSTRAINT_REDUNDANTLY

    public static final int CONSTRAINT_REDUNDANTLY

See Also:
  Constant Field Values

### CONSTRAINT

    public static final int CONSTRAINT

See Also:
  Constant Field Values

### CONSTRUCTOR

    public static final int CONSTRUCTOR

See Also:
  Constant Field Values

### CONTINUES_REDUNDANTLY

    public static final int CONTINUES_REDUNDANTLY

See Also:
  Constant Field Values

### CONTINUES

    public static final int CONTINUES

See Also:
  Constant Field Values

### DECREASES_REDUNDANTLY

    public static final int DECREASES_REDUNDANTLY

See Also:
  Constant Field Values

### DECREASING_REDUNDANTLY

    public static final int DECREASING_REDUNDANTLY

See Also:
  Constant Field Values

### DECREASING

    public static final int DECREASING

See Also:
  Constant Field Values

### DEPENDS_REDUNDANTLY

    public static final int DEPENDS_REDUNDANTLY

See Also:
  Constant Field Values

### DEPENDS

    public static final int DEPENDS

See Also:
  Constant Field Values

### DIVERGES_REDUNDANTLY

    public static final int DIVERGES_REDUNDANTLY

See Also:
  Constant Field Values

### DIVERGES

    public static final int DIVERGES

See Also:
  Constant Field Values

### DURATION_REDUNDANTLY

    public static final int DURATION_REDUNDANTLY

See Also:
  Constant Field Values

### DURATION

    public static final int DURATION

See Also:
  Constant Field Values

### END

    public static final int END

See Also:
  Constant Field Values

### ENSURES_REDUNDANTLY

    public static final int ENSURES_REDUNDANTLY

See Also:
  Constant Field Values

### EXAMPLE

    public static final int EXAMPLE

See Also:
  Constant Field Values

### EXCEPTIONAL_BEHAVIOR

    public static final int EXCEPTIONAL_BEHAVIOR

See Also:
  Constant Field Values

### EXCEPTIONAL_EXAMPLE

    public static final int EXCEPTIONAL_EXAMPLE

See Also:
  Constant Field Values

### EXSURES_REDUNDANTLY

    public static final int EXSURES_REDUNDANTLY

See Also:
  Constant Field Values

### FIELDKW

    public static final int FIELDKW

See Also:
  Constant Field Values

### NO_WACK_FORALL

    public static final int NO_WACK_FORALL

See Also:
  Constant Field Values

### FOR_EXAMPLE

    public static final int FOR_EXAMPLE

See Also:
  Constant Field Values

### IMPLIES_THAT

    public static final int IMPLIES_THAT

See Also:
  Constant Field Values

### HENCE_BY_REDUNDANTLY

    public static final int HENCE_BY_REDUNDANTLY

See Also:
  Constant Field Values

### HENCE_BY

    public static final int HENCE_BY

See Also:
  Constant Field Values

### INITIALIZER

    public static final int INITIALIZER

See Also:
  Constant Field Values

### INITIALLY

    public static final int INITIALLY

See Also:
  Constant Field Values

### INSTANCE

    public static final int INSTANCE

See Also:
  Constant Field Values

### INVARIANT_REDUNDANTLY

    public static final int INVARIANT_REDUNDANTLY

See Also:
  Constant Field Values

### LOOP_INVARIANT_REDUNDANTLY

    public static final int LOOP_INVARIANT_REDUNDANTLY

See Also:
  Constant Field Values

### MAINTAINING_REDUNDANTLY

    public static final int MAINTAINING_REDUNDANTLY

See Also:
  Constant Field Values

### MAINTAINING

    public static final int MAINTAINING

See Also:
  Constant Field Values

### MEASURED_BY_REDUNDANTLY

    public static final int MEASURED_BY_REDUNDANTLY

See Also:
  Constant Field Values

### MEASURED_BY

    public static final int MEASURED_BY

See Also:
  Constant Field Values

### METHOD

    public static final int METHOD

See Also:
  Constant Field Values

### MODEL

    public static final int MODEL

See Also:
  Constant Field Values

### MODEL_PROGRAM

    public static final int MODEL_PROGRAM

See Also:
  Constant Field Values

### MODIFIABLE_REDUNDANTLY

    public static final int MODIFIABLE_REDUNDANTLY

See Also:
  Constant Field Values

### MODIFIABLE

    public static final int MODIFIABLE

See Also:
  Constant Field Values

### MODIFIES_REDUNDANTLY

    public static final int MODIFIES_REDUNDANTLY

See Also:
  Constant Field Values

### NESTEDMODIFIERPRAGMA

    public static final int NESTEDMODIFIERPRAGMA

See Also:
  Constant Field Values

### NORMAL_BEHAVIOR

    public static final int NORMAL_BEHAVIOR

See Also:
  Constant Field Values

### NORMAL_EXAMPLE

    public static final int NORMAL_EXAMPLE

See Also:
  Constant Field Values

### OLD

    public static final int OLD

See Also:
  Constant Field Values

### MODELPROGRAM_OR

    public static final int MODELPROGRAM_OR

See Also:
  Constant Field Values

### PARSEDSPECS

    public static final int PARSEDSPECS

See Also:
  Constant Field Values

### POSTCONDITION_REDUNDANTLY

    public static final int POSTCONDITION_REDUNDANTLY

See Also:
  Constant Field Values

### POSTCONDITION

    public static final int POSTCONDITION

See Also:
  Constant Field Values

### PRECONDITION_REDUNDANTLY

    public static final int PRECONDITION_REDUNDANTLY

See Also:
  Constant Field Values

### PRECONDITION

    public static final int PRECONDITION

See Also:
  Constant Field Values

### PURE

    public static final int PURE

See Also:
  Constant Field Values

### REFINE

    public static final int REFINE

See Also:
  Constant Field Values

### REPRESENTS_REDUNDANTLY

    public static final int REPRESENTS_REDUNDANTLY

See Also:
  Constant Field Values

### REPRESENTS

    public static final int REPRESENTS

See Also:
  Constant Field Values

### REQUIRES_REDUNDANTLY

    public static final int REQUIRES_REDUNDANTLY

See Also:
  Constant Field Values

### RETURNS_REDUNDANTLY

    public static final int RETURNS_REDUNDANTLY

See Also:
  Constant Field Values

### RETURNS

    public static final int RETURNS

See Also:
  Constant Field Values

### SIGNALS_REDUNDANTLY

    public static final int SIGNALS_REDUNDANTLY

See Also:
  Constant Field Values

### SIGNALS

    public static final int SIGNALS

See Also:
  Constant Field Values

### SIGNALS_ONLY

    public static final int SIGNALS_ONLY

See Also:
  Constant Field Values

### SPEC_PROTECTED

    public static final int SPEC_PROTECTED

See Also:
  Constant Field Values

### STATIC_INITIALIZER

    public static final int STATIC_INITIALIZER

See Also:
  Constant Field Values

### SUBCLASSING_CONTRACT

    public static final int SUBCLASSING_CONTRACT

See Also:
  Constant Field Values

### WEAKLY

    public static final int WEAKLY

See Also:
  Constant Field Values

### WHEN_REDUNDANTLY

    public static final int WHEN_REDUNDANTLY

See Also:
  Constant Field Values

### WHEN

    public static final int WHEN

See Also:
  Constant Field Values

### WORKING_SPACE_REDUNDANTLY

    public static final int WORKING_SPACE_REDUNDANTLY

See Also:
  Constant Field Values

### WORKING_SPACE

    public static final int WORKING_SPACE

See Also:
  Constant Field Values

### LASTJMLKEYWORDTAG

    public static final int LASTJMLKEYWORDTAG

See Also:
  Constant Field Values

### FIRSTESCKEYWORDTAG

    public static final int FIRSTESCKEYWORDTAG

See Also:
  Constant Field Values

### ALSO_ENSURES

    public static final int ALSO_ENSURES

See Also:
  Constant Field Values

### ALSO_EXSURES

    public static final int ALSO_EXSURES

See Also:
  Constant Field Values

### ALSO_MODIFIES

    public static final int ALSO_MODIFIES

See Also:
  Constant Field Values

### ALSO_REQUIRES

    public static final int ALSO_REQUIRES

See Also:
  Constant Field Values

### PEER

    public static final int PEER

See Also:
  Constant Field Values

### READONLY

    public static final int READONLY

See Also:
  Constant Field Values

### REP

    public static final int REP

See Also:
  Constant Field Values

### MAY_BE_NULL

    public static final int MAY_BE_NULL

See Also:
  Constant Field Values

### NULL_REF_BY_DEFAULT

    public static final int NULL_REF_BY_DEFAULT

See Also:
  Constant Field Values

### NON_NULL_REF_BY_DEFAULT

    public static final int NON_NULL_REF_BY_DEFAULT

See Also:
  Constant Field Values

### OBS_PURE

    public static final int OBS_PURE

See Also:
  Constant Field Values

### WACK_JAVA_MATH

    public static final int WACK_JAVA_MATH

See Also:
  Constant Field Values

### WACK_SAFE_MATH

    public static final int WACK_SAFE_MATH

See Also:
  Constant Field Values

### WACK_BIGINT_MATH

    public static final int WACK_BIGINT_MATH

See Also:
  Constant Field Values

### CODE_JAVA_MATH

    public static final int CODE_JAVA_MATH

See Also:
  Constant Field Values

### CODE_SAFE_MATH

    public static final int CODE_SAFE_MATH

See Also:
  Constant Field Values

### CODE_BIGINT_MATH

    public static final int CODE_BIGINT_MATH

See Also:
  Constant Field Values

### SPEC_JAVA_MATH

    public static final int SPEC_JAVA_MATH

See Also:
  Constant Field Values

### SPEC_SAFE_MATH

    public static final int SPEC_SAFE_MATH

See Also:
  Constant Field Values

### SPEC_BIGINT_MATH

    public static final int SPEC_BIGINT_MATH

See Also:
  Constant Field Values

### LASTESCKEYWORDTAG

    public static final int LASTESCKEYWORDTAG

See Also:
  Constant Field Values

### LAST_TAG

    public static final int LAST_TAG

See Also:
  Constant Field Values

### ExsuresIdnName

    public static final Identifier ExsuresIdnName

### escchecks

    public static final java.lang.String[] escchecks

### escfunctions

    private static java.lang.String[] escfunctions

### STRINGCATINFIX

    public static final java.lang.String STRINGCATINFIX

See Also:
  Constant Field Values

### jmlkeywords

    private static Identifier[] jmlkeywords

### esckeywords

    private static Identifier[] esckeywords

Constructor Detail

### TagConstants

    public TagConstants()

Method Detail

### toVcString

    public static java.lang.String toVcString(int tag)

### toString

    public static java.lang.String toString(int tag)

### fromIdentifier

    public static int fromIdentifier(Identifier keyword)

  Parameters:
    `keyword` - the keyword to lookup.
  Returns:
    the index of the `TagConstants` attribute corresponding to the keyword encoded as an `Identifier` in the parameter 'keyword'. A `TagConstants.NULL` is returned if the identifier in question is not an ESC/Java or JML keyword known to `TagConstants`.

### isKeywordTag

    public static boolean isKeywordTag(int tag)

### checkFromString

    public static int checkFromString(java.lang.String s)

### makeRedundant

    public static int makeRedundant(int tag)

  Returns:
    a "redundant-fied" version of the passed tag if it can be made redundant; otherwise, return the parameter unchanged.

### unRedundant

    public static int unRedundant(int tag)

  Returns:
    an "unredundant-fied" version of the passed tag if it is redundant; otherwise, return the parameter unchanged.

### isRedundant

    public static boolean isRedundant(int tag)

### main

    public static void main(java.lang.String[] args)

### comp

    private static void comp(int i,
                             int j,
                             java.lang.String s)

Overview | Package | Class | Use | Tree | Deprecated | Index | Help
| ESC/Java2 © 2003,2004,2005 David Cok and Joseph Kiniry © 2005 UCD Dublin © 2003,2004 Radboud University Nijmegen © 1999,2000 Compaq Computer Corporation © 1997,1998,1999 Digital Equipment Corporation All Rights Reserved
PREV CLASS NEXT CLASS | FRAMES NO FRAMES
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD

The ESC/Java2 Project Homepage