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

escjava.ast
Class TagConstants

java.lang.Object
  extended byjavafe.ast.GeneratedTags
      extended byjavafe.ast.OperatorTags
          extended byjavafe.ast.TagConstants
              extended byjavafe.parser.TagConstants
                  extended byjavafe.tc.TagConstants
                      extended byescjava.ast.GeneratedTags
                          extended byescjava.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)

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

The ESC/Java2 Project Homepage