KeYJMLLexer (KeY API Documentation)

java.lang.Object
- org.antlr.runtime.BaseRecognizer
- - org.antlr.runtime.Lexer
  - - de.uka.ilkd.key.speclang.jml.translation.KeYJMLLexer

All Implemented Interfaces:: org.antlr.runtime.TokenSource

public class KeYJMLLexer
extends org.antlr.runtime.Lexer

Nested Class Summary

Nested Classes
Modifier and Type Class and Description

protected class KeYJMLLexer.DFA29

Nested Classes
Modifier and Type	Class and Description
`protected class`	`KeYJMLLexer.DFA29`

Field Summary

Fields
Modifier and Type	Field and Description
`static int`	`ACCESSIBLE`
`static int`	`ALLFIELDS`
`static int`	`ALLOBJECTS`
`static int`	`AND`
`static int`	`ASSIGNABLE`
`static int`	`BACKSLASH_PREFIXED`
`static int`	`BACKUP`
`static int`	`BEFORE`
`static int`	`BIGINT`
`static int`	`BINDIGIT`
`static int`	`BINLITERAL`
`static int`	`BINPREFIX`
`static int`	`BITWISENOT`
`static int`	`BOOLEAN`
`static int`	`BREAKS`
`static int`	`BSUM`
`static int`	`BY`
`static int`	`BYTE`
`static int`	`CHAR_LITERAL`
`static int`	`COLON`
`static int`	`COMMA`
`static int`	`CONTINUES`
`static int`	`DECDIGIT`
`static int`	`DECLASSIFIES`
`static int`	`DECLITERAL`
`static int`	`DECREASES`
`static int`	`DEPENDS`
`static int`	`DETERMINES`
`protected KeYJMLLexer.DFA29`	`dfa29`
`(package private) static short[]`	`DFA29_accept`
`(package private) static java.lang.String`	`DFA29_acceptS`
`(package private) static short[]`	`DFA29_eof`
`(package private) static java.lang.String`	`DFA29_eofS`
`(package private) static short[]`	`DFA29_eot`
`(package private) static java.lang.String`	`DFA29_eotS`
`(package private) static char[]`	`DFA29_max`
`(package private) static java.lang.String`	`DFA29_maxS`
`(package private) static char[]`	`DFA29_min`
`(package private) static java.lang.String`	`DFA29_minS`
`(package private) static short[]`	`DFA29_special`
`(package private) static java.lang.String`	`DFA29_specialS`
`(package private) static short[][]`	`DFA29_transition`
`(package private) static java.lang.String[]`	`DFA29_transitionS`
`static int`	`DIGIT`
`static int`	`DISJOINT`
`static int`	`DIV`
`static int`	`DL_ESCAPE`
`static int`	`DOC_COMMENT`
`static int`	`DOMAIN_IMPLIES_CREATED`
`static int`	`DOT`
`static int`	`DOTDOT`
`static int`	`DURATION`
`static int`	`ELEMTYPE`
`static int`	`EMPTYSET`
`static int`	`ENSURES`
`static int`	`ENSURES_FREE`
`static int`	`EOF`
`static int`	`EQ_NEQ`
`static int`	`EQUAL_SINGLE`
`static int`	`EQV_ANTIV`
`static int`	`ERASES`
`static int`	`ESC`
`static int`	`EVERYTHING`
`static int`	`EXCEPTION`
`static int`	`EXISTS`
`static int`	`FALSE`
`static int`	`FORALL`
`static int`	`FREE`
`static int`	`FRESH`
`static int`	`GEQ`
`static int`	`GT`
`static int`	`HEXDIGIT`
`static int`	`HEXLITERAL`
`static int`	`HEXPREFIX`
`static int`	`IDENT`
`static int`	`IMPLIES`
`static int`	`IMPLIESBACKWARD`
`static int`	`IN_DOMAIN`
`static int`	`INCLUSIVEOR`
`static int`	`INDEX`
`static int`	`INDEXOF`
`static int`	`INFORMAL_DESCRIPTION`
`static int`	`INSTANCEOF`
`static int`	`INT`
`static int`	`INTERSECT`
`static int`	`INTO`
`static int`	`INV`
`static int`	`INVARIANT_FOR`
`static int`	`IS_FINITE`
`static int`	`IS_INITIALIZED`
`static int`	`ITSELF`
`static int`	`JML_IDENT`
`static int`	`LARROW`
`static int`	`LBLNEG`
`static int`	`LBLPOS`
`static int`	`LBRACE`
`static int`	`LBRACKET`
`static int`	`LEQ`
`static int`	`LETTER`
`static int`	`LETTERORDIGIT`
`static int`	`LOCKSET`
`static int`	`LOCKSET_LEQ`
`static int`	`LOCKSET_LT`
`static int`	`LOCSET`
`static int`	`LOGICALAND`
`static int`	`LOGICALOR`
`static int`	`LONG`
`static int`	`LONGSUFFIX`
`static int`	`LOOP_DETERMINES`
`static int`	`LOOP_SEPARATES`
`static int`	`LPAREN`
`static int`	`LT`
`static int`	`LT_IMPLICIT_GT_DISPATCH`
`static int`	`MAP`
`static int`	`MAP_GET`
`static int`	`MAP_OVERRIDE`
`static int`	`MAP_REMOVE`
`static int`	`MAP_SINGLETON`
`static int`	`MAP_SIZE`
`static int`	`MAP_UPDATE`
`static int`	`MAPEMPTY`
`static int`	`MAX`
`static int`	`MEASURED_BY`
`static int`	`MERGE_PARAMS`
`static int`	`MIN`
`static int`	`MINUS`
`static int`	`MOD`
`static int`	`MODEL_METHOD_AXIOM`
`static int`	`MULT`
`static int`	`NEW`
`static int`	`NEW_OBJECTS`
`static int`	`NEWELEMSFRESH`
`static int`	`NON_NULL`
`static int`	`NONNULLELEMENTS`
`static int`	`NONZERODECDIGIT`
`static int`	`NOT`
`static int`	`NOT_ASSIGNED`
`static int`	`NOT_MODIFIED`
`static int`	`NOT_SPECIFIED`
`static int`	`NOTHING`
`static int`	`NULL`
`static int`	`NULLABLE`
`static int`	`NUM_OF`
`static int`	`OCT_CHAR`
`static int`	`OCTDIGIT`
`static int`	`OCTLITERAL`
`static int`	`OCTPREFIX`
`static int`	`OLD`
`static int`	`PERMISSION`
`static int`	`PLUS`
`static int`	`PRAGMA`
`static int`	`PRE`
`static int`	`PRODUCT`
`static int`	`QUESTIONMARK`
`static int`	`RARROW`
`static int`	`RBRACE`
`static int`	`RBRACKET`
`static int`	`REACH`
`static int`	`REACHLOCS`
`static int`	`REAL`
`static int`	`REPRESENTS`
`static int`	`REQUIRES`
`static int`	`REQUIRES_FREE`
`static int`	`RESULT`
`static int`	`RETURNS`
`static int`	`RPAREN`
`static int`	`SAME`
`static int`	`SEMI`
`static int`	`SEPARATES`
`static int`	`SEQ`
`static int`	`SEQ2MAP`
`static int`	`SEQCONCAT`
`static int`	`SEQDEF`
`static int`	`SEQEMPTY`
`static int`	`SEQGET`
`static int`	`SEQREPLACE`
`static int`	`SEQREVERSE`
`static int`	`SEQSINGLETON`
`static int`	`SEQSUB`
`static int`	`SETMINUS`
`static int`	`SHIFTLEFT`
`static int`	`SHIFTRIGHT`
`static int`	`SHORT`
`static int`	`SIGNALS`
`static int`	`SIGNALS_ONLY`
`static int`	`SINGLETON`
`static int`	`SL_COMMENT`
`static int`	`SPACE`
`static int`	`ST`
`static int`	`STATIC_INVARIANT_FOR`
`static int`	`STRICTLY_NOTHING`
`static int`	`STRING_EQUAL`
`static int`	`STRING_LITERAL`
`static int`	`SUBSET`
`static int`	`SUCH_THAT`
`static int`	`SUM`
`static int`	`SUPER`
`static int`	`THIS`
`static int`	`TRANSACTIONUPDATED`
`static int`	`TRANSIENT`
`static int`	`TRUE`
`static int`	`TYPE`
`static int`	`TYPE_SMALL`
`static int`	`TYPEOF`
`static int`	`UNION`
`static int`	`UNIONINF`
`static int`	`UNSIGNEDSHIFTRIGHT`
`static int`	`VALUES`
`static int`	`VOID`
`static int`	`WORKINGSPACE`
`static int`	`WS`
`static int`	`XOR`

Fields inherited from class org.antlr.runtime.Lexer
input

Fields inherited from class org.antlr.runtime.BaseRecognizer
DEFAULT_TOKEN_CHANNEL, HIDDEN, INITIAL_FOLLOW_STACK_SIZE, MEMO_RULE_FAILED, MEMO_RULE_UNKNOWN, NEXT_TOKEN_RULE_NAME, state

Constructor Summary

Constructors
Constructor and Description
`KeYJMLLexer()`
`KeYJMLLexer(org.antlr.runtime.CharStream input)`
`KeYJMLLexer(org.antlr.runtime.CharStream input, org.antlr.runtime.RecognizerSharedState state)`

Method Summary

All Methods Instance Methods Concrete Methods
Modifier and Type	Method and Description
`org.antlr.runtime.Lexer[]`	`getDelegates()`
`java.lang.String`	`getGrammarFileName()`
`void`	`mACCESSIBLE()`
`void`	`mALLFIELDS()`
`void`	`mALLOBJECTS()`
`void`	`mAND()`
`void`	`mASSIGNABLE()`
`void`	`mBACKSLASH_PREFIXED()`
`void`	`mBACKUP()`
`void`	`mBEFORE()`
`void`	`mBIGINT()`
`void`	`mBINDIGIT()`
`void`	`mBINLITERAL()`
`void`	`mBINPREFIX()`
`void`	`mBITWISENOT()`
`void`	`mBOOLEAN()`
`void`	`mBREAKS()`
`void`	`mBSUM()`
`void`	`mBY()`
`void`	`mBYTE()`
`void`	`mCHAR_LITERAL()`
`void`	`mCOLON()`
`void`	`mCOMMA()`
`void`	`mCONTINUES()`
`void`	`mDECDIGIT()`
`void`	`mDECLASSIFIES()`
`void`	`mDECLITERAL()`
`void`	`mDECREASES()`
`void`	`mDEPENDS()`
`void`	`mDETERMINES()`
`void`	`mDIGIT()`
`void`	`mDISJOINT()`
`void`	`mDIV()`
`void`	`mDL_ESCAPE()`
`void`	`mDOC_COMMENT()`
`void`	`mDOMAIN_IMPLIES_CREATED()`
`void`	`mDOT()`
`void`	`mDOTDOT()`
`void`	`mDURATION()`
`void`	`mELEMTYPE()`
`void`	`mEMPTYSET()`
`void`	`mENSURES_FREE()`
`void`	`mENSURES()`
`void`	`mEQ_NEQ()`
`void`	`mEQUAL_SINGLE()`
`void`	`mEQV_ANTIV()`
`void`	`mERASES()`
`void`	`mESC()`
`void`	`mEVERYTHING()`
`void`	`mEXCEPTION()`
`void`	`mEXISTS()`
`void`	`mFALSE()`
`void`	`mFORALL()`
`void`	`mFREE()`
`void`	`mFRESH()`
`void`	`mGEQ()`
`void`	`mGT()`
`void`	`mHEXDIGIT()`
`void`	`mHEXLITERAL()`
`void`	`mHEXPREFIX()`
`void`	`mIDENT()`
`void`	`mIMPLIES()`
`void`	`mIMPLIESBACKWARD()`
`void`	`mIN_DOMAIN()`
`void`	`mINCLUSIVEOR()`
`void`	`mINDEX()`
`void`	`mINDEXOF()`
`void`	`mINFORMAL_DESCRIPTION()`
`void`	`mINSTANCEOF()`
`void`	`mINT()`
`void`	`mINTERSECT()`
`void`	`mINTO()`
`void`	`mINV()`
`void`	`mINVARIANT_FOR()`
`void`	`mIS_FINITE()`
`void`	`mIS_INITIALIZED()`
`void`	`mITSELF()`
`void`	`mJML_IDENT()`
`void`	`mLARROW()`
`void`	`mLBLNEG()`
`void`	`mLBLPOS()`
`void`	`mLBRACE()`
`void`	`mLBRACKET()`
`void`	`mLEQ()`
`void`	`mLETTER()`
`void`	`mLETTERORDIGIT()`
`void`	`mLOCKSET_LEQ()`
`void`	`mLOCKSET_LT()`
`void`	`mLOCKSET()`
`void`	`mLOCSET()`
`void`	`mLOGICALAND()`
`void`	`mLOGICALOR()`
`void`	`mLONG()`
`void`	`mLONGSUFFIX()`
`void`	`mLOOP_DETERMINES()`
`void`	`mLOOP_SEPARATES()`
`void`	`mLPAREN()`
`void`	`mLT_IMPLICIT_GT_DISPATCH()`
`void`	`mLT()`
`void`	`mMAP_GET()`
`void`	`mMAP_OVERRIDE()`
`void`	`mMAP_REMOVE()`
`void`	`mMAP_SINGLETON()`
`void`	`mMAP_SIZE()`
`void`	`mMAP_UPDATE()`
`void`	`mMAP()`
`void`	`mMAPEMPTY()`
`void`	`mMAX()`
`void`	`mMEASURED_BY()`
`void`	`mMERGE_PARAMS()`
`void`	`mMIN()`
`void`	`mMINUS()`
`void`	`mMOD()`
`void`	`mMODEL_METHOD_AXIOM()`
`void`	`mMULT()`
`void`	`mNEW_OBJECTS()`
`void`	`mNEW()`
`void`	`mNEWELEMSFRESH()`
`void`	`mNON_NULL()`
`void`	`mNONNULLELEMENTS()`
`void`	`mNONZERODECDIGIT()`
`void`	`mNOT_ASSIGNED()`
`void`	`mNOT_MODIFIED()`
`void`	`mNOT_SPECIFIED()`
`void`	`mNOT()`
`void`	`mNOTHING()`
`void`	`mNULL()`
`void`	`mNULLABLE()`
`void`	`mNUM_OF()`
`void`	`mOCT_CHAR()`
`void`	`mOCTDIGIT()`
`void`	`mOCTLITERAL()`
`void`	`mOCTPREFIX()`
`void`	`mOLD()`
`void`	`mPERMISSION()`
`void`	`mPLUS()`
`void`	`mPRAGMA()`
`void`	`mPRE()`
`void`	`mPRODUCT()`
`void`	`mQUESTIONMARK()`
`void`	`mRARROW()`
`void`	`mRBRACE()`
`void`	`mRBRACKET()`
`void`	`mREACH()`
`void`	`mREACHLOCS()`
`void`	`mREAL()`
`void`	`mREPRESENTS()`
`void`	`mREQUIRES_FREE()`
`void`	`mREQUIRES()`
`void`	`mRESULT()`
`void`	`mRETURNS()`
`void`	`mRPAREN()`
`void`	`mSAME()`
`void`	`mSEMI()`
`void`	`mSEPARATES()`
`void`	`mSEQ()`
`void`	`mSEQ2MAP()`
`void`	`mSEQCONCAT()`
`void`	`mSEQDEF()`
`void`	`mSEQEMPTY()`
`void`	`mSEQGET()`
`void`	`mSEQREPLACE()`
`void`	`mSEQREVERSE()`
`void`	`mSEQSINGLETON()`
`void`	`mSEQSUB()`
`void`	`mSETMINUS()`
`void`	`mSHIFTLEFT()`
`void`	`mSHIFTRIGHT()`
`void`	`mSHORT()`
`void`	`mSIGNALS_ONLY()`
`void`	`mSIGNALS()`
`void`	`mSINGLETON()`
`void`	`mSL_COMMENT()`
`void`	`mSPACE()`
`void`	`mST()`
`void`	`mSTATIC_INVARIANT_FOR()`
`void`	`mSTRICTLY_NOTHING()`
`void`	`mSTRING_EQUAL()`
`void`	`mSTRING_LITERAL()`
`void`	`mSUBSET()`
`void`	`mSUCH_THAT()`
`void`	`mSUM()`
`void`	`mSUPER()`
`void`	`mTHIS()`
`void`	`mTokens()`
`void`	`mTRANSACTIONUPDATED()`
`void`	`mTRANSIENT()`
`void`	`mTRUE()`
`void`	`mTYPE_SMALL()`
`void`	`mTYPE()`
`void`	`mTYPEOF()`
`void`	`mUNION()`
`void`	`mUNIONINF()`
`void`	`mUNSIGNEDSHIFTRIGHT()`
`void`	`mVALUES()`
`void`	`mVOID()`
`void`	`mWORKINGSPACE()`
`void`	`mWS()`
`void`	`mXOR()`
`void`	`reportError(org.antlr.runtime.RecognitionException e)`
`void`	`synpred1_KeYJMLLexer_fragment()`
`boolean`	`synpred1_KeYJMLLexer()`
`void`	`synpred2_KeYJMLLexer_fragment()`
`boolean`	`synpred2_KeYJMLLexer()`
`void`	`synpred3_KeYJMLLexer_fragment()`
`boolean`	`synpred3_KeYJMLLexer()`

Methods inherited from class org.antlr.runtime.Lexer
emit, emit, getCharErrorDisplay, getCharIndex, getCharPositionInLine, getCharStream, getEOFToken, getErrorMessage, getLine, getSourceName, getText, match, match, matchAny, matchRange, nextToken, recover, reset, setCharStream, setText, skip, traceIn, traceOut

Methods inherited from class org.antlr.runtime.BaseRecognizer
alreadyParsedRule, beginResync, combineFollows, computeContextSensitiveRuleFOLLOW, computeErrorRecoverySet, consumeUntil, consumeUntil, displayRecognitionError, emitErrorMessage, endResync, failed, getBacktrackingLevel, getCurrentInputSymbol, getErrorHeader, getMissingSymbol, getNumberOfSyntaxErrors, getRuleInvocationStack, getRuleInvocationStack, getRuleMemoization, getRuleMemoizationCacheSize, getTokenErrorDisplay, getTokenNames, match, matchAny, memoize, mismatchIsMissingToken, mismatchIsUnwantedToken, pushFollow, recover, recoverFromMismatchedSet, recoverFromMismatchedToken, setBacktrackingLevel, toStrings, traceIn, traceOut

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

Field Detail
- EOF
```
public static final int EOF
```
  See Also:
  
  Constant Field Values
- ACCESSIBLE
```
public static final int ACCESSIBLE
```
  See Also:
  
  Constant Field Values
- ALLFIELDS
```
public static final int ALLFIELDS
```
  See Also:
  
  Constant Field Values
- ALLOBJECTS
```
public static final int ALLOBJECTS
```
  See Also:
  
  Constant Field Values
- AND
```
public static final int AND
```
  See Also:
  
  Constant Field Values
- ASSIGNABLE
```
public static final int ASSIGNABLE
```
  See Also:
  
  Constant Field Values
- BACKSLASH_PREFIXED
```
public static final int BACKSLASH_PREFIXED
```
  See Also:
  
  Constant Field Values
- BACKUP
```
public static final int BACKUP
```
  See Also:
  
  Constant Field Values
- BEFORE
```
public static final int BEFORE
```
  See Also:
  
  Constant Field Values
- BIGINT
```
public static final int BIGINT
```
  See Also:
  
  Constant Field Values
- BINDIGIT
```
public static final int BINDIGIT
```
  See Also:
  
  Constant Field Values
- BINLITERAL
```
public static final int BINLITERAL
```
  See Also:
  
  Constant Field Values
- BINPREFIX
```
public static final int BINPREFIX
```
  See Also:
  
  Constant Field Values
- BITWISENOT
```
public static final int BITWISENOT
```
  See Also:
  
  Constant Field Values
- BOOLEAN
```
public static final int BOOLEAN
```
  See Also:
  
  Constant Field Values
- BREAKS
```
public static final int BREAKS
```
  See Also:
  
  Constant Field Values
- BSUM
```
public static final int BSUM
```
  See Also:
  
  Constant Field Values
- BY
```
public static final int BY
```
  See Also:
  
  Constant Field Values
- BYTE
```
public static final int BYTE
```
  See Also:
  
  Constant Field Values
- CHAR_LITERAL
```
public static final int CHAR_LITERAL
```
  See Also:
  
  Constant Field Values
- COLON
```
public static final int COLON
```
  See Also:
  
  Constant Field Values
- COMMA
```
public static final int COMMA
```
  See Also:
  
  Constant Field Values
- CONTINUES
```
public static final int CONTINUES
```
  See Also:
  
  Constant Field Values
- DECDIGIT
```
public static final int DECDIGIT
```
  See Also:
  
  Constant Field Values
- DECLASSIFIES
```
public static final int DECLASSIFIES
```
  See Also:
  
  Constant Field Values
- DECLITERAL
```
public static final int DECLITERAL
```
  See Also:
  
  Constant Field Values
- DECREASES
```
public static final int DECREASES
```
  See Also:
  
  Constant Field Values
- DEPENDS
```
public static final int DEPENDS
```
  See Also:
  
  Constant Field Values
- DETERMINES
```
public static final int DETERMINES
```
  See Also:
  
  Constant Field Values
- DIGIT
```
public static final int DIGIT
```
  See Also:
  
  Constant Field Values
- DISJOINT
```
public static final int DISJOINT
```
  See Also:
  
  Constant Field Values
- DIV
```
public static final int DIV
```
  See Also:
  
  Constant Field Values
- DL_ESCAPE
```
public static final int DL_ESCAPE
```
  See Also:
  
  Constant Field Values
- DOC_COMMENT
```
public static final int DOC_COMMENT
```
  See Also:
  
  Constant Field Values
- DOMAIN_IMPLIES_CREATED
```
public static final int DOMAIN_IMPLIES_CREATED
```
  See Also:
  
  Constant Field Values
- DOT
```
public static final int DOT
```
  See Also:
  
  Constant Field Values
- DOTDOT
```
public static final int DOTDOT
```
  See Also:
  
  Constant Field Values
- DURATION
```
public static final int DURATION
```
  See Also:
  
  Constant Field Values
- ELEMTYPE
```
public static final int ELEMTYPE
```
  See Also:
  
  Constant Field Values
- EMPTYSET
```
public static final int EMPTYSET
```
  See Also:
  
  Constant Field Values
- ENSURES
```
public static final int ENSURES
```
  See Also:
  
  Constant Field Values
- ENSURES_FREE
```
public static final int ENSURES_FREE
```
  See Also:
  
  Constant Field Values
- EQUAL_SINGLE
```
public static final int EQUAL_SINGLE
```
  See Also:
  
  Constant Field Values
- EQV_ANTIV
```
public static final int EQV_ANTIV
```
  See Also:
  
  Constant Field Values
- EQ_NEQ
```
public static final int EQ_NEQ
```
  See Also:
  
  Constant Field Values
- ERASES
```
public static final int ERASES
```
  See Also:
  
  Constant Field Values
- ESC
```
public static final int ESC
```
  See Also:
  
  Constant Field Values
- EVERYTHING
```
public static final int EVERYTHING
```
  See Also:
  
  Constant Field Values
- EXCEPTION
```
public static final int EXCEPTION
```
  See Also:
  
  Constant Field Values
- EXISTS
```
public static final int EXISTS
```
  See Also:
  
  Constant Field Values
- FALSE
```
public static final int FALSE
```
  See Also:
  
  Constant Field Values
- FORALL
```
public static final int FORALL
```
  See Also:
  
  Constant Field Values
- FREE
```
public static final int FREE
```
  See Also:
  
  Constant Field Values
- FRESH
```
public static final int FRESH
```
  See Also:
  
  Constant Field Values
- GEQ
```
public static final int GEQ
```
  See Also:
  
  Constant Field Values
- GT
```
public static final int GT
```
  See Also:
  
  Constant Field Values
- HEXDIGIT
```
public static final int HEXDIGIT
```
  See Also:
  
  Constant Field Values
- HEXLITERAL
```
public static final int HEXLITERAL
```
  See Also:
  
  Constant Field Values
- HEXPREFIX
```
public static final int HEXPREFIX
```
  See Also:
  
  Constant Field Values
- IDENT
```
public static final int IDENT
```
  See Also:
  
  Constant Field Values
- IMPLIES
```
public static final int IMPLIES
```
  See Also:
  
  Constant Field Values
- IMPLIESBACKWARD
```
public static final int IMPLIESBACKWARD
```
  See Also:
  
  Constant Field Values
- INCLUSIVEOR
```
public static final int INCLUSIVEOR
```
  See Also:
  
  Constant Field Values
- INDEX
```
public static final int INDEX
```
  See Also:
  
  Constant Field Values
- INDEXOF
```
public static final int INDEXOF
```
  See Also:
  
  Constant Field Values
- INFORMAL_DESCRIPTION
```
public static final int INFORMAL_DESCRIPTION
```
  See Also:
  
  Constant Field Values
- INSTANCEOF
```
public static final int INSTANCEOF
```
  See Also:
  
  Constant Field Values
- INT
```
public static final int INT
```
  See Also:
  
  Constant Field Values
- INTERSECT
```
public static final int INTERSECT
```
  See Also:
  
  Constant Field Values
- INTO
```
public static final int INTO
```
  See Also:
  
  Constant Field Values
- INV
```
public static final int INV
```
  See Also:
  
  Constant Field Values
- INVARIANT_FOR
```
public static final int INVARIANT_FOR
```
  See Also:
  
  Constant Field Values
- IN_DOMAIN
```
public static final int IN_DOMAIN
```
  See Also:
  
  Constant Field Values
- IS_FINITE
```
public static final int IS_FINITE
```
  See Also:
  
  Constant Field Values
- IS_INITIALIZED
```
public static final int IS_INITIALIZED
```
  See Also:
  
  Constant Field Values
- ITSELF
```
public static final int ITSELF
```
  See Also:
  
  Constant Field Values
- JML_IDENT
```
public static final int JML_IDENT
```
  See Also:
  
  Constant Field Values
- LARROW
```
public static final int LARROW
```
  See Also:
  
  Constant Field Values
- LBLNEG
```
public static final int LBLNEG
```
  See Also:
  
  Constant Field Values
- LBLPOS
```
public static final int LBLPOS
```
  See Also:
  
  Constant Field Values
- LBRACE
```
public static final int LBRACE
```
  See Also:
  
  Constant Field Values
- LBRACKET
```
public static final int LBRACKET
```
  See Also:
  
  Constant Field Values
- LEQ
```
public static final int LEQ
```
  See Also:
  
  Constant Field Values
- LETTER
```
public static final int LETTER
```
  See Also:
  
  Constant Field Values
- LETTERORDIGIT
```
public static final int LETTERORDIGIT
```
  See Also:
  
  Constant Field Values
- LOCKSET
```
public static final int LOCKSET
```
  See Also:
  
  Constant Field Values
- LOCKSET_LEQ
```
public static final int LOCKSET_LEQ
```
  See Also:
  
  Constant Field Values
- LOCKSET_LT
```
public static final int LOCKSET_LT
```
  See Also:
  
  Constant Field Values
- LOCSET
```
public static final int LOCSET
```
  See Also:
  
  Constant Field Values
- LOGICALAND
```
public static final int LOGICALAND
```
  See Also:
  
  Constant Field Values
- LOGICALOR
```
public static final int LOGICALOR
```
  See Also:
  
  Constant Field Values
- LONG
```
public static final int LONG
```
  See Also:
  
  Constant Field Values
- LONGSUFFIX
```
public static final int LONGSUFFIX
```
  See Also:
  
  Constant Field Values
- LOOP_DETERMINES
```
public static final int LOOP_DETERMINES
```
  See Also:
  
  Constant Field Values
- LOOP_SEPARATES
```
public static final int LOOP_SEPARATES
```
  See Also:
  
  Constant Field Values
- LPAREN
```
public static final int LPAREN
```
  See Also:
  
  Constant Field Values
- LT
```
public static final int LT
```
  See Also:
  
  Constant Field Values
- LT_IMPLICIT_GT_DISPATCH
```
public static final int LT_IMPLICIT_GT_DISPATCH
```
  See Also:
  
  Constant Field Values
- MAP
```
public static final int MAP
```
  See Also:
  
  Constant Field Values
- MAPEMPTY
```
public static final int MAPEMPTY
```
  See Also:
  
  Constant Field Values
- MAP_GET
```
public static final int MAP_GET
```
  See Also:
  
  Constant Field Values
- MAP_OVERRIDE
```
public static final int MAP_OVERRIDE
```
  See Also:
  
  Constant Field Values
- MAP_REMOVE
```
public static final int MAP_REMOVE
```
  See Also:
  
  Constant Field Values
- MAP_SINGLETON
```
public static final int MAP_SINGLETON
```
  See Also:
  
  Constant Field Values
- MAP_SIZE
```
public static final int MAP_SIZE
```
  See Also:
  
  Constant Field Values
- MAP_UPDATE
```
public static final int MAP_UPDATE
```
  See Also:
  
  Constant Field Values
- MAX
```
public static final int MAX
```
  See Also:
  
  Constant Field Values
- MEASURED_BY
```
public static final int MEASURED_BY
```
  See Also:
  
  Constant Field Values
- MERGE_PARAMS
```
public static final int MERGE_PARAMS
```
  See Also:
  
  Constant Field Values
- MIN
```
public static final int MIN
```
  See Also:
  
  Constant Field Values
- MINUS
```
public static final int MINUS
```
  See Also:
  
  Constant Field Values
- MOD
```
public static final int MOD
```
  See Also:
  
  Constant Field Values
- MODEL_METHOD_AXIOM
```
public static final int MODEL_METHOD_AXIOM
```
  See Also:
  
  Constant Field Values
- MULT
```
public static final int MULT
```
  See Also:
  
  Constant Field Values
- NEW
```
public static final int NEW
```
  See Also:
  
  Constant Field Values
- NEWELEMSFRESH
```
public static final int NEWELEMSFRESH
```
  See Also:
  
  Constant Field Values
- NEW_OBJECTS
```
public static final int NEW_OBJECTS
```
  See Also:
  
  Constant Field Values
- NONNULLELEMENTS
```
public static final int NONNULLELEMENTS
```
  See Also:
  
  Constant Field Values
- NONZERODECDIGIT
```
public static final int NONZERODECDIGIT
```
  See Also:
  
  Constant Field Values
- NON_NULL
```
public static final int NON_NULL
```
  See Also:
  
  Constant Field Values
- NOT
```
public static final int NOT
```
  See Also:
  
  Constant Field Values
- NOTHING
```
public static final int NOTHING
```
  See Also:
  
  Constant Field Values
- NOT_ASSIGNED
```
public static final int NOT_ASSIGNED
```
  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
- NULL
```
public static final int NULL
```
  See Also:
  
  Constant Field Values
- NULLABLE
```
public static final int NULLABLE
```
  See Also:
  
  Constant Field Values
- NUM_OF
```
public static final int NUM_OF
```
  See Also:
  
  Constant Field Values
- OCTDIGIT
```
public static final int OCTDIGIT
```
  See Also:
  
  Constant Field Values
- OCTLITERAL
```
public static final int OCTLITERAL
```
  See Also:
  
  Constant Field Values
- OCTPREFIX
```
public static final int OCTPREFIX
```
  See Also:
  
  Constant Field Values
- OCT_CHAR
```
public static final int OCT_CHAR
```
  See Also:
  
  Constant Field Values
- OLD
```
public static final int OLD
```
  See Also:
  
  Constant Field Values
- PERMISSION
```
public static final int PERMISSION
```
  See Also:
  
  Constant Field Values
- PLUS
```
public static final int PLUS
```
  See Also:
  
  Constant Field Values
- PRAGMA
```
public static final int PRAGMA
```
  See Also:
  
  Constant Field Values
- PRE
```
public static final int PRE
```
  See Also:
  
  Constant Field Values
- PRODUCT
```
public static final int PRODUCT
```
  See Also:
  
  Constant Field Values
- QUESTIONMARK
```
public static final int QUESTIONMARK
```
  See Also:
  
  Constant Field Values
- RARROW
```
public static final int RARROW
```
  See Also:
  
  Constant Field Values
- RBRACE
```
public static final int RBRACE
```
  See Also:
  
  Constant Field Values
- RBRACKET
```
public static final int RBRACKET
```
  See Also:
  
  Constant Field Values
- REACH
```
public static final int REACH
```
  See Also:
  
  Constant Field Values
- REACHLOCS
```
public static final int REACHLOCS
```
  See Also:
  
  Constant Field Values
- REAL
```
public static final int REAL
```
  See Also:
  
  Constant Field Values
- REPRESENTS
```
public static final int REPRESENTS
```
  See Also:
  
  Constant Field Values
- REQUIRES
```
public static final int REQUIRES
```
  See Also:
  
  Constant Field Values
- REQUIRES_FREE
```
public static final int REQUIRES_FREE
```
  See Also:
  
  Constant Field Values
- RESULT
```
public static final int RESULT
```
  See Also:
  
  Constant Field Values
- RETURNS
```
public static final int RETURNS
```
  See Also:
  
  Constant Field Values
- RPAREN
```
public static final int RPAREN
```
  See Also:
  
  Constant Field Values
- SAME
```
public static final int SAME
```
  See Also:
  
  Constant Field Values
- SEMI
```
public static final int SEMI
```
  See Also:
  
  Constant Field Values
- SEPARATES
```
public static final int SEPARATES
```
  See Also:
  
  Constant Field Values
- SEQ
```
public static final int SEQ
```
  See Also:
  
  Constant Field Values
- SEQ2MAP
```
public static final int SEQ2MAP
```
  See Also:
  
  Constant Field Values
- SEQCONCAT
```
public static final int SEQCONCAT
```
  See Also:
  
  Constant Field Values
- SEQDEF
```
public static final int SEQDEF
```
  See Also:
  
  Constant Field Values
- SEQEMPTY
```
public static final int SEQEMPTY
```
  See Also:
  
  Constant Field Values
- SEQGET
```
public static final int SEQGET
```
  See Also:
  
  Constant Field Values
- SEQREPLACE
```
public static final int SEQREPLACE
```
  See Also:
  
  Constant Field Values
- SEQREVERSE
```
public static final int SEQREVERSE
```
  See Also:
  
  Constant Field Values
- SEQSINGLETON
```
public static final int SEQSINGLETON
```
  See Also:
  
  Constant Field Values
- SEQSUB
```
public static final int SEQSUB
```
  See Also:
  
  Constant Field Values
- SETMINUS
```
public static final int SETMINUS
```
  See Also:
  
  Constant Field Values
- SHIFTLEFT
```
public static final int SHIFTLEFT
```
  See Also:
  
  Constant Field Values
- SHIFTRIGHT
```
public static final int SHIFTRIGHT
```
  See Also:
  
  Constant Field Values
- SHORT
```
public static final int SHORT
```
  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
- SINGLETON
```
public static final int SINGLETON
```
  See Also:
  
  Constant Field Values
- SL_COMMENT
```
public static final int SL_COMMENT
```
  See Also:
  
  Constant Field Values
- SPACE
```
public static final int SPACE
```
  See Also:
  
  Constant Field Values
- ST
```
public static final int ST
```
  See Also:
  
  Constant Field Values
- STATIC_INVARIANT_FOR
```
public static final int STATIC_INVARIANT_FOR
```
  See Also:
  
  Constant Field Values
- STRICTLY_NOTHING
```
public static final int STRICTLY_NOTHING
```
  See Also:
  
  Constant Field Values
- STRING_EQUAL
```
public static final int STRING_EQUAL
```
  See Also:
  
  Constant Field Values
- STRING_LITERAL
```
public static final int STRING_LITERAL
```
  See Also:
  
  Constant Field Values
- SUBSET
```
public static final int SUBSET
```
  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
- SUPER
```
public static final int SUPER
```
  See Also:
  
  Constant Field Values
- THIS
```
public static final int THIS
```
  See Also:
  
  Constant Field Values
- TRANSACTIONUPDATED
```
public static final int TRANSACTIONUPDATED
```
  See Also:
  
  Constant Field Values
- TRANSIENT
```
public static final int TRANSIENT
```
  See Also:
  
  Constant Field Values
- TRUE
```
public static final int TRUE
```
  See Also:
  
  Constant Field Values
- TYPE
```
public static final int TYPE
```
  See Also:
  
  Constant Field Values
- TYPEOF
```
public static final int TYPEOF
```
  See Also:
  
  Constant Field Values
- TYPE_SMALL
```
public static final int TYPE_SMALL
```
  See Also:
  
  Constant Field Values
- UNION
```
public static final int UNION
```
  See Also:
  
  Constant Field Values
- UNIONINF
```
public static final int UNIONINF
```
  See Also:
  
  Constant Field Values
- UNSIGNEDSHIFTRIGHT
```
public static final int UNSIGNEDSHIFTRIGHT
```
  See Also:
  
  Constant Field Values
- VALUES
```
public static final int VALUES
```
  See Also:
  
  Constant Field Values
- VOID
```
public static final int VOID
```
  See Also:
  
  Constant Field Values
- WORKINGSPACE
```
public static final int WORKINGSPACE
```
  See Also:
  
  Constant Field Values
- WS
```
public static final int WS
```
  See Also:
  
  Constant Field Values
- XOR
```
public static final int XOR
```
  See Also:
  
  Constant Field Values
- dfa29
```
protected KeYJMLLexer.DFA29 dfa29
```
- DFA29_eotS
```
static final java.lang.String DFA29_eotS
```
  See Also:
  
  Constant Field Values
- DFA29_eofS
```
static final java.lang.String DFA29_eofS
```
  See Also:
  
  Constant Field Values
- DFA29_minS
```
static final java.lang.String DFA29_minS
```
  See Also:
  
  Constant Field Values
- DFA29_maxS
```
static final java.lang.String DFA29_maxS
```
  See Also:
  
  Constant Field Values
- DFA29_acceptS
```
static final java.lang.String DFA29_acceptS
```
  See Also:
  
  Constant Field Values
- DFA29_specialS
```
static final java.lang.String DFA29_specialS
```
  See Also:
  
  Constant Field Values
- DFA29_transitionS
```
static final java.lang.String[] DFA29_transitionS
```
- DFA29_eot
```
static final short[] DFA29_eot
```
- DFA29_eof
```
static final short[] DFA29_eof
```
- DFA29_min
```
static final char[] DFA29_min
```
- DFA29_max
```
static final char[] DFA29_max
```
- DFA29_accept
```
static final short[] DFA29_accept
```
- DFA29_special
```
static final short[] DFA29_special
```
- DFA29_transition
```
static final short[][] DFA29_transition
```

Constructor Detail

KeYJMLLexer
```
public KeYJMLLexer()
```

KeYJMLLexer

public KeYJMLLexer(org.antlr.runtime.CharStream input)

KeYJMLLexer

public KeYJMLLexer(org.antlr.runtime.CharStream input,
                   org.antlr.runtime.RecognizerSharedState state)

Method Detail

reportError

public void reportError(org.antlr.runtime.RecognitionException e)

Overrides:: reportError in class org.antlr.runtime.Lexer

getDelegates

public org.antlr.runtime.Lexer[] getDelegates()

getGrammarFileName
```
public java.lang.String getGrammarFileName()
```
Overrides:

getGrammarFileName in class org.antlr.runtime.BaseRecognizer

mBOOLEAN

public final void mBOOLEAN()
                    throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mBYTE

public final void mBYTE()
                 throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mFALSE

public final void mFALSE()
                  throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mINSTANCEOF

public final void mINSTANCEOF()
                       throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mINT

public final void mINT()
                throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mLONG

public final void mLONG()
                 throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mNEW

public final void mNEW()
                throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mNULL

public final void mNULL()
                 throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mSHORT

public final void mSHORT()
                  throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mSUPER

public final void mSUPER()
                  throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mTHIS

public final void mTHIS()
                 throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mTRUE

public final void mTRUE()
                 throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mVOID

public final void mVOID()
                 throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mACCESSIBLE

public final void mACCESSIBLE()
                       throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mASSIGNABLE

public final void mASSIGNABLE()
                       throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mBREAKS

public final void mBREAKS()
                   throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mCONTINUES

public final void mCONTINUES()
                      throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mDECREASES

public final void mDECREASES()
                      throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mDEPENDS

public final void mDEPENDS()
                    throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mDETERMINES

public final void mDETERMINES()
                       throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mENSURES

public final void mENSURES()
                    throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mENSURES_FREE

public final void mENSURES_FREE()
                         throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mLOOP_DETERMINES

public final void mLOOP_DETERMINES()
                            throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mLOOP_SEPARATES

public final void mLOOP_SEPARATES()
                           throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mMODEL_METHOD_AXIOM

public final void mMODEL_METHOD_AXIOM()
                               throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mMERGE_PARAMS

public final void mMERGE_PARAMS()
                         throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mNON_NULL

public final void mNON_NULL()
                     throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mNULLABLE

public final void mNULLABLE()
                     throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mREPRESENTS

public final void mREPRESENTS()
                       throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mREQUIRES

public final void mREQUIRES()
                     throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mREQUIRES_FREE

public final void mREQUIRES_FREE()
                          throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mRETURNS

public final void mRETURNS()
                    throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mSEPARATES

public final void mSEPARATES()
                      throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mSIGNALS

public final void mSIGNALS()
                    throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mSIGNALS_ONLY

public final void mSIGNALS_ONLY()
                         throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mALLFIELDS

public final void mALLFIELDS()
                      throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mALLOBJECTS

public final void mALLOBJECTS()
                       throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mBACKUP

public final void mBACKUP()
                   throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mBEFORE

public final void mBEFORE()
                   throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mBIGINT

public final void mBIGINT()
                   throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mBSUM

public final void mBSUM()
                 throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mBY

public final void mBY()
               throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mDECLASSIFIES

public final void mDECLASSIFIES()
                         throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mDISJOINT

public final void mDISJOINT()
                     throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mDOMAIN_IMPLIES_CREATED

public final void mDOMAIN_IMPLIES_CREATED()
                                   throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mDURATION

public final void mDURATION()
                     throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mELEMTYPE

public final void mELEMTYPE()
                     throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mEMPTYSET

public final void mEMPTYSET()
                     throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mERASES

public final void mERASES()
                   throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mEVERYTHING

public final void mEVERYTHING()
                       throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mEXCEPTION

public final void mEXCEPTION()
                      throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mEXISTS

public final void mEXISTS()
                   throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mFORALL

public final void mFORALL()
                   throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mFREE

public final void mFREE()
                 throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mFRESH

public final void mFRESH()
                  throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mINDEX

public final void mINDEX()
                  throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mINDEXOF

public final void mINDEXOF()
                    throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mINTERSECT

public final void mINTERSECT()
                      throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mINTO

public final void mINTO()
                 throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mINV

public final void mINV()
                throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mINVARIANT_FOR

public final void mINVARIANT_FOR()
                          throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mIN_DOMAIN

public final void mIN_DOMAIN()
                      throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mIS_FINITE

public final void mIS_FINITE()
                      throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mIS_INITIALIZED

public final void mIS_INITIALIZED()
                           throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mITSELF

public final void mITSELF()
                   throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mLBLNEG

public final void mLBLNEG()
                   throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mLBLPOS

public final void mLBLPOS()
                   throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mLOCKSET

public final void mLOCKSET()
                    throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mLOCSET

public final void mLOCSET()
                   throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mMAP

public final void mMAP()
                throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mMAPEMPTY

public final void mMAPEMPTY()
                     throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mMAP_GET

public final void mMAP_GET()
                    throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mMAP_OVERRIDE

public final void mMAP_OVERRIDE()
                         throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mMAP_REMOVE

public final void mMAP_REMOVE()
                       throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mMAP_SINGLETON

public final void mMAP_SINGLETON()
                          throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mMAP_SIZE

public final void mMAP_SIZE()
                     throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mMAP_UPDATE

public final void mMAP_UPDATE()
                       throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mMAX

public final void mMAX()
                throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mMEASURED_BY

public final void mMEASURED_BY()
                        throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mMIN

public final void mMIN()
                throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mNEWELEMSFRESH

public final void mNEWELEMSFRESH()
                          throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mNEW_OBJECTS

public final void mNEW_OBJECTS()
                        throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mNONNULLELEMENTS

public final void mNONNULLELEMENTS()
                            throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mNOTHING

public final void mNOTHING()
                    throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mNOT_ASSIGNED

public final void mNOT_ASSIGNED()
                         throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mNOT_MODIFIED

public final void mNOT_MODIFIED()
                         throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mNOT_SPECIFIED

public final void mNOT_SPECIFIED()
                          throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mNUM_OF

public final void mNUM_OF()
                   throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mOLD

public final void mOLD()
                throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mPERMISSION

public final void mPERMISSION()
                       throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mPRE

public final void mPRE()
                throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mPRODUCT

public final void mPRODUCT()
                    throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mREACH

public final void mREACH()
                  throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mREACHLOCS

public final void mREACHLOCS()
                      throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mREAL

public final void mREAL()
                 throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mRESULT

public final void mRESULT()
                   throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mSAME

public final void mSAME()
                 throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mSEQ

public final void mSEQ()
                throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mSEQ2MAP

public final void mSEQ2MAP()
                    throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mSEQCONCAT

public final void mSEQCONCAT()
                      throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mSEQDEF

public final void mSEQDEF()
                   throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mSEQEMPTY

public final void mSEQEMPTY()
                     throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mSEQGET

public final void mSEQGET()
                   throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mSEQREPLACE

public final void mSEQREPLACE()
                       throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mSEQREVERSE

public final void mSEQREVERSE()
                       throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mSEQSINGLETON

public final void mSEQSINGLETON()
                         throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mSEQSUB

public final void mSEQSUB()
                   throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mSETMINUS

public final void mSETMINUS()
                     throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mSINGLETON

public final void mSINGLETON()
                      throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mSPACE

public final void mSPACE()
                  throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mSTATIC_INVARIANT_FOR

public final void mSTATIC_INVARIANT_FOR()
                                 throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mSTRICTLY_NOTHING

public final void mSTRICTLY_NOTHING()
                             throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mSTRING_EQUAL

public final void mSTRING_EQUAL()
                         throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mSUBSET

public final void mSUBSET()
                   throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mSUCH_THAT

public final void mSUCH_THAT()
                      throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mSUM

public final void mSUM()
                throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mTRANSACTIONUPDATED

public final void mTRANSACTIONUPDATED()
                               throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mTRANSIENT

public final void mTRANSIENT()
                      throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mTYPE

public final void mTYPE()
                 throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mTYPEOF

public final void mTYPEOF()
                   throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mTYPE_SMALL

public final void mTYPE_SMALL()
                       throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mUNION

public final void mUNION()
                  throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mUNIONINF

public final void mUNIONINF()
                     throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mVALUES

public final void mVALUES()
                   throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mWORKINGSPACE

public final void mWORKINGSPACE()
                         throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mAND

public final void mAND()
                throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mBITWISENOT

public final void mBITWISENOT()
                       throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mCOLON

public final void mCOLON()
                  throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mCOMMA

public final void mCOMMA()
                  throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mDIV

public final void mDIV()
                throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mDOT

public final void mDOT()
                throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mDOTDOT

public final void mDOTDOT()
                   throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mEQUAL_SINGLE

public final void mEQUAL_SINGLE()
                         throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mEQV_ANTIV

public final void mEQV_ANTIV()
                      throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mEQ_NEQ

public final void mEQ_NEQ()
                   throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mGEQ

public final void mGEQ()
                throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mIMPLIES

public final void mIMPLIES()
                    throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mIMPLIESBACKWARD

public final void mIMPLIESBACKWARD()
                            throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mINCLUSIVEOR

public final void mINCLUSIVEOR()
                        throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mLARROW

public final void mLARROW()
                   throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mLBRACE

public final void mLBRACE()
                   throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mLEQ

public final void mLEQ()
                throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mLOCKSET_LEQ

public final void mLOCKSET_LEQ()
                        throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mLOCKSET_LT

public final void mLOCKSET_LT()
                       throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mLOGICALAND

public final void mLOGICALAND()
                       throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mLOGICALOR

public final void mLOGICALOR()
                      throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mMINUS

public final void mMINUS()
                  throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mMOD

public final void mMOD()
                throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mMULT

public final void mMULT()
                 throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mNOT

public final void mNOT()
                throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mPLUS

public final void mPLUS()
                 throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mQUESTIONMARK

public final void mQUESTIONMARK()
                         throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mRARROW

public final void mRARROW()
                   throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mRBRACE

public final void mRBRACE()
                   throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mSEMI

public final void mSEMI()
                 throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mSHIFTLEFT

public final void mSHIFTLEFT()
                      throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mSHIFTRIGHT

public final void mSHIFTRIGHT()
                       throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mST

public final void mST()
               throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mUNSIGNEDSHIFTRIGHT

public final void mUNSIGNEDSHIFTRIGHT()
                               throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mXOR

public final void mXOR()
                throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mGT

public final void mGT()
               throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mLT

public final void mLT()
               throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mLT_IMPLICIT_GT_DISPATCH

public final void mLT_IMPLICIT_GT_DISPATCH()
                                    throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mLPAREN

public final void mLPAREN()
                   throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mRPAREN

public final void mRPAREN()
                   throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mLBRACKET

public final void mLBRACKET()
                     throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mRBRACKET

public final void mRBRACKET()
                     throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mLETTER

public final void mLETTER()
                   throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mBINDIGIT

public final void mBINDIGIT()
                     throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mOCTDIGIT

public final void mOCTDIGIT()
                     throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mNONZERODECDIGIT

public final void mNONZERODECDIGIT()
                            throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mDECDIGIT

public final void mDECDIGIT()
                     throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mDIGIT

public final void mDIGIT()
                  throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mHEXDIGIT

public final void mHEXDIGIT()
                     throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mBINPREFIX

public final void mBINPREFIX()
                      throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mOCTPREFIX

public final void mOCTPREFIX()
                      throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mHEXPREFIX

public final void mHEXPREFIX()
                      throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mLONGSUFFIX

public final void mLONGSUFFIX()
                       throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mBINLITERAL

public final void mBINLITERAL()
                       throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mOCTLITERAL

public final void mOCTLITERAL()
                       throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mDECLITERAL

public final void mDECLITERAL()
                       throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mHEXLITERAL

public final void mHEXLITERAL()
                       throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mLETTERORDIGIT

public final void mLETTERORDIGIT()
                          throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mIDENT

public final void mIDENT()
                  throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mJML_IDENT

public final void mJML_IDENT()
                      throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mDL_ESCAPE

public final void mDL_ESCAPE()
                      throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mBACKSLASH_PREFIXED

public final void mBACKSLASH_PREFIXED()
                               throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mCHAR_LITERAL

public final void mCHAR_LITERAL()
                         throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mOCT_CHAR

public final void mOCT_CHAR()
                     throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mSTRING_LITERAL

public final void mSTRING_LITERAL()
                           throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mESC

public final void mESC()
                throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mWS

public final void mWS()
               throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mINFORMAL_DESCRIPTION

public final void mINFORMAL_DESCRIPTION()
                                 throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mSL_COMMENT

public final void mSL_COMMENT()
                       throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mDOC_COMMENT

public final void mDOC_COMMENT()
                        throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mPRAGMA

public final void mPRAGMA()
                   throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

mTokens
```
public void mTokens()
             throws org.antlr.runtime.RecognitionException
```
Specified by:

mTokens in class org.antlr.runtime.Lexer

Throws:

org.antlr.runtime.RecognitionException

synpred1_KeYJMLLexer_fragment

public final void synpred1_KeYJMLLexer_fragment()
                                         throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

synpred2_KeYJMLLexer_fragment

public final void synpred2_KeYJMLLexer_fragment()
                                         throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

synpred3_KeYJMLLexer_fragment

public final void synpred3_KeYJMLLexer_fragment()
                                         throws org.antlr.runtime.RecognitionException

Throws:: org.antlr.runtime.RecognitionException

synpred1_KeYJMLLexer

public final boolean synpred1_KeYJMLLexer()

synpred3_KeYJMLLexer

public final boolean synpred3_KeYJMLLexer()

synpred2_KeYJMLLexer

public final boolean synpred2_KeYJMLLexer()

Class KeYJMLLexer

Nested Class Summary

Field Summary

Fields inherited from class org.antlr.runtime.Lexer

Fields inherited from class org.antlr.runtime.BaseRecognizer

Constructor Summary

Method Summary

Methods inherited from class org.antlr.runtime.Lexer

Methods inherited from class org.antlr.runtime.BaseRecognizer

Methods inherited from class java.lang.Object

Field Detail

EOF

ACCESSIBLE

ALLFIELDS

ALLOBJECTS

AND

ASSIGNABLE

BACKSLASH_PREFIXED

BACKUP

BEFORE

BIGINT

BINDIGIT

BINLITERAL

BINPREFIX

BITWISENOT

BOOLEAN

BREAKS

BSUM

BY

BYTE

CHAR_LITERAL

COLON

COMMA

CONTINUES

DECDIGIT

DECLASSIFIES

DECLITERAL

DECREASES

DEPENDS

DETERMINES

DIGIT

DISJOINT

DIV

DL_ESCAPE

DOC_COMMENT

DOMAIN_IMPLIES_CREATED

DOT

DOTDOT

DURATION

ELEMTYPE

EMPTYSET

ENSURES

ENSURES_FREE

EQUAL_SINGLE

EQV_ANTIV

EQ_NEQ

ERASES

ESC

EVERYTHING

EXCEPTION

EXISTS

FALSE

FORALL

FREE

FRESH

GEQ

GT

HEXDIGIT

HEXLITERAL

HEXPREFIX

IDENT

IMPLIES

IMPLIESBACKWARD

INCLUSIVEOR

INDEX

INDEXOF

INFORMAL_DESCRIPTION

INSTANCEOF

INT

INTERSECT