public class KeYParser
extends org.antlr.v4.runtime.Parser
Modifier and Type | Field and Description |
---|---|
static org.antlr.v4.runtime.atn.ATN |
_ATN |
protected static org.antlr.v4.runtime.dfa.DFA[] |
_decisionToDFA |
static java.lang.String |
_serializedATN |
protected static org.antlr.v4.runtime.atn.PredictionContextCache |
_sharedContextCache |
static int |
ABSTRACT |
static int |
ADD |
static int |
ADDPROGVARS |
static int |
ADDRULES |
static int |
AND |
static int |
ANTECEDENTPOLARITY |
static int |
APPLY_UPDATE_ON_RIGID |
static int |
ASSIGN |
static int |
ASSUMES |
static int |
AT |
static int |
AVOID |
static int |
AXIOMS |
static int |
BIN_LITERAL |
static int |
BOOTCLASSPATH |
static int |
CHAR_LITERAL |
static int |
CHOOSECONTRACT |
static int |
CLASSPATH |
static int |
CLOSEGOAL |
static int |
COLON |
static int |
COMMA |
static int |
COMMENT_END |
static int |
CONTAINERTYPE |
static int |
CONTAINS_ASSIGNMENT |
static int |
CONTRACTS |
static int |
DEPENDINGON |
static int |
DIFFERENT |
static int |
DIFFERENTFIELDS |
static int |
DISJOINTMODULONULL |
static int |
DISPLAYNAME |
static int |
DOC_COMMENT |
static int |
DOT |
static int |
DOTRANGE |
static int |
DOUBLECOLON |
static int |
DROP_EFFECTLESS_ELEMENTARIES |
static int |
DROP_EFFECTLESS_STORES |
static int |
ELEMSORT |
static int |
ELSE |
static int |
EMPTYBRACKETS |
static int |
ENUM_CONST |
static int |
EQUAL_UNIQUE |
static int |
EQUALS |
static int |
EQV |
static int |
ERROR_CHAR |
static int |
EXISTS |
static int |
EXP |
static int |
EXTENDS |
static int |
FALSE |
static int |
FIELDTYPE |
static int |
FINAL |
static int |
FIND |
static int |
FORALL |
static int |
FORMULA |
static int |
FREELABELIN |
static int |
FUNCTIONS |
static int |
GENERIC |
static int |
GET_FREE_INVARIANT |
static int |
GET_INVARIANT |
static int |
GET_VARIANT |
static int |
GREATER |
static int |
GREATEREQUAL |
static int |
HAS_ELEMENTARY_SORT |
static int |
HAS_INVARIANT |
static int |
HASLABEL |
static int |
HASSORT |
static int |
HASSUBFORMULAS |
static int |
HELPTEXT |
static int |
HEURISTICS |
static int |
HEURISTICSDECL |
static int |
HEX_LITERAL |
static int |
IDENT |
static int |
IF |
static int |
IFEX |
static int |
IMP |
static int |
IN_TYPE |
static int |
INCLUDE |
static int |
INCLUDELDTS |
static int |
INSEQUENTSTATE |
static int |
INSTANTIATE_GENERIC |
static int |
INVARIANTS |
static int |
IS_ABSTRACT_OR_INTERFACE |
static int |
IS_LABELED |
static int |
ISARRAY |
static int |
ISARRAYLENGTH |
static int |
ISCONSTANT |
static int |
ISENUMTYPE |
static int |
ISINDUCTVAR |
static int |
ISLOCALVARIABLE |
static int |
ISOBSERVER |
static int |
ISREFERENCE |
static int |
ISREFERENCEARRAY |
static int |
ISSTATICFIELD |
static int |
ISSUBTYPE |
static int |
ISTHISREFERENCE |
static int |
JAVASOURCE |
static int |
KEYSETTINGS |
static int |
LBRACE |
static int |
LBRACKET |
static int |
LEMMA |
static int |
LESS |
static int |
LESSEQUAL |
static int |
LGUILLEMETS |
static int |
LPAREN |
static int |
MAXEXPANDMETHOD |
static int |
METADISJOINT |
static int |
MINUS |
static int |
ML_COMMENT |
static int |
MODAILITYGENERIC1 |
static int |
MODAILITYGENERIC2 |
static int |
MODAILITYGENERIC3 |
static int |
MODAILITYGENERIC4 |
static int |
MODAILITYGENERIC5 |
static int |
MODAILITYGENERIC6 |
static int |
MODAILITYGENERIC7 |
static int |
MODALITY |
static int |
MODALITYB |
static int |
MODALITYB_END |
static int |
MODALITYBB |
static int |
MODALITYBB_END |
static int |
MODALITYD |
static int |
MODALITYD_CHAR |
static int |
MODALITYD_END |
static int |
MODALITYD_STRING |
static int |
MODALITYG_END |
static int |
MODALOPERATOR |
static int |
MODIFIES |
static int |
NEW |
static int |
NEW_DEPENDING_ON |
static int |
NEW_TYPE_OF |
static int |
NEWLABEL |
static int |
NODEFAULTCLASSES |
static int |
NONINTERACTIVE |
static int |
NOT |
static int |
NOT_ |
static int |
NOT_EQUALS |
static int |
NOTFREEIN |
static int |
NUM_LITERAL |
static int |
ONEOF |
static int |
OPTIONSDECL |
static int |
OR |
static int |
PARALLEL |
static int |
PERCENT |
static int |
PLUS |
static int |
PREDICATES |
static int |
PRIMES |
static int |
PROBLEM |
static int |
PROFILE |
static int |
PROGRAM |
static int |
PROGRAMVARIABLES |
static int |
PROOF |
static int |
PROOFOBLIGATION |
static int |
PROOFSCRIPT |
static int |
PROXY |
static int |
QUOTED_STRING_LITERAL |
static int |
RBRACE |
static int |
RBRACKET |
static int |
REPLACEWITH |
static int |
RGUILLEMETS |
static int |
RPAREN |
static int |
RULE_abbreviation |
static int |
RULE_accessterm |
static int |
RULE_activated_choice |
static int |
RULE_add |
static int |
RULE_addprogvar |
static int |
RULE_addrules |
static int |
RULE_arg_sorts |
static int |
RULE_arg_sorts_or_formula |
static int |
RULE_arg_sorts_or_formula_helper |
static int |
RULE_argument_list |
static int |
RULE_arrayopid |
static int |
RULE_atom_prefix |
static int |
RULE_attribute |
static int |
RULE_boolean_literal |
static int |
RULE_bootClassPath |
static int |
RULE_bound_variables |
static int |
RULE_brace_suffix |
static int |
RULE_bracket_suffix_heap |
static int |
RULE_bracket_term |
static int |
RULE_call |
static int |
RULE_cast_term |
static int |
RULE_char_literal |
static int |
RULE_choice |
static int |
RULE_classPaths |
static int |
RULE_comparison_term |
static int |
RULE_conjunction_term |
static int |
RULE_contracts |
static int |
RULE_decls |
static int |
RULE_disjunction_term |
static int |
RULE_elementary_update_term |
static int |
RULE_equality_term |
static int |
RULE_equivalence_term |
static int |
RULE_extends_sorts |
static int |
RULE_file |
static int |
RULE_func_decl |
static int |
RULE_func_decls |
static int |
RULE_funcpred_name |
static int |
RULE_goalspec |
static int |
RULE_goalspecs |
static int |
RULE_goalspecwithoption |
static int |
RULE_id_declaration |
static int |
RULE_ifExThenElseTerm |
static int |
RULE_ifThenElseTerm |
static int |
RULE_implication_term |
static int |
RULE_invariants |
static int |
RULE_javaSource |
static int |
RULE_keyjavatype |
static int |
RULE_label |
static int |
RULE_literals |
static int |
RULE_location_term |
static int |
RULE_locset_term |
static int |
RULE_metaId |
static int |
RULE_metaTerm |
static int |
RULE_modifiers |
static int |
RULE_number |
static int |
RULE_one_bound_variable |
static int |
RULE_one_contract |
static int |
RULE_one_include |
static int |
RULE_one_include_statement |
static int |
RULE_one_invariant |
static int |
RULE_one_schema_modal_op_decl |
static int |
RULE_one_schema_var_decl |
static int |
RULE_one_sort_decl |
static int |
RULE_oneJavaSource |
static int |
RULE_oneof_sorts |
static int |
RULE_option |
static int |
RULE_option_decls |
static int |
RULE_option_list |
static int |
RULE_optionDecl |
static int |
RULE_options_choice |
static int |
RULE_parallel_term |
static int |
RULE_pred_decl |
static int |
RULE_pred_decls |
static int |
RULE_preferences |
static int |
RULE_primitive_labeled_term |
static int |
RULE_primitive_term |
static int |
RULE_problem |
static int |
RULE_profile |
static int |
RULE_prog_var_decls |
static int |
RULE_proof |
static int |
RULE_proofScript |
static int |
RULE_pvset |
static int |
RULE_replacewith |
static int |
RULE_ruleset |
static int |
RULE_ruleset_decls |
static int |
RULE_rulesets |
static int |
RULE_rulesOrAxioms |
static int |
RULE_schema_modifiers |
static int |
RULE_schema_var_decls |
static int |
RULE_semisequent |
static int |
RULE_seq |
static int |
RULE_seqEOF |
static int |
RULE_simple_ident |
static int |
RULE_simple_ident_comma_list |
static int |
RULE_simple_ident_dots |
static int |
RULE_simple_ident_dots_comma_list |
static int |
RULE_single_label |
static int |
RULE_sort_decls |
static int |
RULE_sortId |
static int |
RULE_string_literal |
static int |
RULE_string_value |
static int |
RULE_strong_arith_term_1 |
static int |
RULE_strong_arith_term_2 |
static int |
RULE_substitution_term |
static int |
RULE_taclet |
static int |
RULE_tacletlist |
static int |
RULE_term |
static int |
RULE_term60 |
static int |
RULE_termEOF |
static int |
RULE_termorseq |
static int |
RULE_termParen |
static int |
RULE_transform_decl |
static int |
RULE_transform_decls |
static int |
RULE_triggers |
static int |
RULE_unary_formula |
static int |
RULE_unary_minus_term |
static int |
RULE_update_term |
static int |
RULE_varexp |
static int |
RULE_varexp_argument |
static int |
RULE_varexpId |
static int |
RULE_varexplist |
static int |
RULE_varId |
static int |
RULE_varIds |
static int |
RULE_weak_arith_term |
static int |
RULE_where_to_bind |
static java.lang.String[] |
ruleNames |
static int |
RULES |
static int |
SAME |
static int |
SAME_OBSERVER |
static int |
SAMEUPDATELEVEL |
static int |
SCHEMAVAR |
static int |
SCHEMAVARIABLES |
static int |
SEMI |
static int |
SEQARROW |
static int |
SIMPLIFY_IF_THEN_ELSE_UPDATE |
static int |
SKOLEMFORMULA |
static int |
SKOLEMTERM |
static int |
SL_COMMENT |
static int |
SLASH |
static int |
SORTS |
static int |
STAR |
static int |
STATIC |
static int |
STATICMETHODREFERENCE |
static int |
STORE_STMT_IN |
static int |
STORE_TERM_IN |
static int |
STRICT |
static int |
STRING_LITERAL |
static int |
SUBST |
static int |
SUCCEDENTPOLARITY |
static int |
TERM |
static int |
TERMLABEL |
static int |
THEN |
static int |
TILDE |
static java.lang.String[] |
tokenNames
Deprecated.
Use
VOCABULARY instead. |
static int |
TRANSFORMERS |
static int |
TRIGGER |
static int |
TRUE |
static int |
TYPEOF |
static int |
UNIQUE |
static int |
UPDATE |
static int |
UTF_EMPTY |
static int |
UTF_IN |
static int |
UTF_INTERSECT |
static int |
UTF_PRECEDES |
static int |
UTF_SETMINUS |
static int |
UTF_SUBSET |
static int |
UTF_UNION |
static int |
VARCOND |
static int |
VARIABLE |
static int |
VARIABLES |
static org.antlr.v4.runtime.Vocabulary |
VOCABULARY |
static int |
WITHOPTIONS |
static int |
WS |
Constructor and Description |
---|
KeYParser(org.antlr.v4.runtime.TokenStream input) |
addContextToParseTree, addParseListener, compileParseTreePattern, compileParseTreePattern, consume, createErrorNode, createTerminalNode, dumpDFA, enterOuterAlt, enterRecursionRule, enterRecursionRule, enterRule, exitRule, getATNWithBypassAlts, getBuildParseTree, getContext, getCurrentToken, getDFAStrings, getErrorHandler, getExpectedTokens, getExpectedTokensWithinCurrentRule, getInputStream, getInvokingContext, getNumberOfSyntaxErrors, getParseInfo, getParseListeners, getPrecedence, getRuleContext, getRuleIndex, getRuleInvocationStack, getRuleInvocationStack, getSourceName, getTokenFactory, getTokenStream, getTrimParseTree, inContext, isExpectedToken, isMatchedEOF, isTrace, match, matchWildcard, notifyErrorListeners, notifyErrorListeners, precpred, pushNewRecursionContext, removeParseListener, removeParseListeners, reset, setBuildParseTree, setContext, setErrorHandler, setInputStream, setProfile, setTokenFactory, setTokenStream, setTrace, setTrimParseTree, triggerEnterRuleEvent, triggerExitRuleEvent, unrollRecursionContexts
action, addErrorListener, getErrorHeader, getErrorListenerDispatch, getErrorListeners, getInterpreter, getRuleIndexMap, getState, getTokenErrorDisplay, getTokenType, getTokenTypeMap, removeErrorListener, removeErrorListeners, sempred, setInterpreter, setState
protected static final org.antlr.v4.runtime.dfa.DFA[] _decisionToDFA
protected static final org.antlr.v4.runtime.atn.PredictionContextCache _sharedContextCache
public static final int MODALITY
public static final int SORTS
public static final int GENERIC
public static final int PROXY
public static final int EXTENDS
public static final int ONEOF
public static final int ABSTRACT
public static final int SCHEMAVARIABLES
public static final int SCHEMAVAR
public static final int MODALOPERATOR
public static final int PROGRAM
public static final int FORMULA
public static final int TERM
public static final int UPDATE
public static final int VARIABLES
public static final int VARIABLE
public static final int SKOLEMTERM
public static final int SKOLEMFORMULA
public static final int TERMLABEL
public static final int MODIFIES
public static final int PROGRAMVARIABLES
public static final int STORE_TERM_IN
public static final int STORE_STMT_IN
public static final int HAS_INVARIANT
public static final int GET_INVARIANT
public static final int GET_FREE_INVARIANT
public static final int GET_VARIANT
public static final int IS_LABELED
public static final int SAME_OBSERVER
public static final int VARCOND
public static final int APPLY_UPDATE_ON_RIGID
public static final int DEPENDINGON
public static final int DISJOINTMODULONULL
public static final int DROP_EFFECTLESS_ELEMENTARIES
public static final int DROP_EFFECTLESS_STORES
public static final int SIMPLIFY_IF_THEN_ELSE_UPDATE
public static final int ENUM_CONST
public static final int FREELABELIN
public static final int HASSORT
public static final int FIELDTYPE
public static final int FINAL
public static final int ELEMSORT
public static final int HASLABEL
public static final int HASSUBFORMULAS
public static final int ISARRAY
public static final int ISARRAYLENGTH
public static final int ISCONSTANT
public static final int ISENUMTYPE
public static final int ISINDUCTVAR
public static final int ISLOCALVARIABLE
public static final int ISOBSERVER
public static final int DIFFERENT
public static final int METADISJOINT
public static final int ISTHISREFERENCE
public static final int DIFFERENTFIELDS
public static final int ISREFERENCE
public static final int ISREFERENCEARRAY
public static final int ISSTATICFIELD
public static final int ISSUBTYPE
public static final int EQUAL_UNIQUE
public static final int NEW
public static final int NEW_TYPE_OF
public static final int NEW_DEPENDING_ON
public static final int HAS_ELEMENTARY_SORT
public static final int NEWLABEL
public static final int CONTAINS_ASSIGNMENT
public static final int NOT_
public static final int NOTFREEIN
public static final int SAME
public static final int STATIC
public static final int STATICMETHODREFERENCE
public static final int MAXEXPANDMETHOD
public static final int STRICT
public static final int TYPEOF
public static final int INSTANTIATE_GENERIC
public static final int FORALL
public static final int EXISTS
public static final int SUBST
public static final int IF
public static final int IFEX
public static final int THEN
public static final int ELSE
public static final int INCLUDE
public static final int INCLUDELDTS
public static final int CLASSPATH
public static final int BOOTCLASSPATH
public static final int NODEFAULTCLASSES
public static final int JAVASOURCE
public static final int WITHOPTIONS
public static final int OPTIONSDECL
public static final int KEYSETTINGS
public static final int PROFILE
public static final int TRUE
public static final int FALSE
public static final int SAMEUPDATELEVEL
public static final int INSEQUENTSTATE
public static final int ANTECEDENTPOLARITY
public static final int SUCCEDENTPOLARITY
public static final int CLOSEGOAL
public static final int HEURISTICSDECL
public static final int NONINTERACTIVE
public static final int DISPLAYNAME
public static final int HELPTEXT
public static final int REPLACEWITH
public static final int ADDRULES
public static final int ADDPROGVARS
public static final int HEURISTICS
public static final int FIND
public static final int ADD
public static final int ASSUMES
public static final int TRIGGER
public static final int AVOID
public static final int PREDICATES
public static final int FUNCTIONS
public static final int TRANSFORMERS
public static final int UNIQUE
public static final int RULES
public static final int AXIOMS
public static final int PROBLEM
public static final int CHOOSECONTRACT
public static final int PROOFOBLIGATION
public static final int PROOF
public static final int PROOFSCRIPT
public static final int CONTRACTS
public static final int INVARIANTS
public static final int LEMMA
public static final int IN_TYPE
public static final int IS_ABSTRACT_OR_INTERFACE
public static final int CONTAINERTYPE
public static final int UTF_PRECEDES
public static final int UTF_IN
public static final int UTF_EMPTY
public static final int UTF_UNION
public static final int UTF_INTERSECT
public static final int UTF_SUBSET
public static final int UTF_SETMINUS
public static final int SEMI
public static final int SLASH
public static final int COLON
public static final int DOUBLECOLON
public static final int ASSIGN
public static final int DOT
public static final int DOTRANGE
public static final int COMMA
public static final int LPAREN
public static final int RPAREN
public static final int LBRACE
public static final int RBRACE
public static final int LBRACKET
public static final int RBRACKET
public static final int EMPTYBRACKETS
public static final int AT
public static final int PARALLEL
public static final int OR
public static final int AND
public static final int NOT
public static final int IMP
public static final int EQUALS
public static final int NOT_EQUALS
public static final int SEQARROW
public static final int EXP
public static final int TILDE
public static final int PERCENT
public static final int STAR
public static final int MINUS
public static final int PLUS
public static final int GREATER
public static final int GREATEREQUAL
public static final int RGUILLEMETS
public static final int WS
public static final int STRING_LITERAL
public static final int LESS
public static final int LESSEQUAL
public static final int LGUILLEMETS
public static final int EQV
public static final int PRIMES
public static final int CHAR_LITERAL
public static final int QUOTED_STRING_LITERAL
public static final int SL_COMMENT
public static final int BIN_LITERAL
public static final int HEX_LITERAL
public static final int IDENT
public static final int NUM_LITERAL
public static final int ERROR_CHAR
public static final int COMMENT_END
public static final int DOC_COMMENT
public static final int ML_COMMENT
public static final int MODALITYD
public static final int MODALITYB
public static final int MODALITYBB
public static final int MODAILITYGENERIC1
public static final int MODAILITYGENERIC2
public static final int MODAILITYGENERIC3
public static final int MODAILITYGENERIC4
public static final int MODAILITYGENERIC5
public static final int MODAILITYGENERIC6
public static final int MODAILITYGENERIC7
public static final int MODALITYD_END
public static final int MODALITYD_STRING
public static final int MODALITYD_CHAR
public static final int MODALITYG_END
public static final int MODALITYB_END
public static final int MODALITYBB_END
public static final int RULE_file
public static final int RULE_decls
public static final int RULE_problem
public static final int RULE_one_include_statement
public static final int RULE_one_include
public static final int RULE_options_choice
public static final int RULE_activated_choice
public static final int RULE_option_decls
public static final int RULE_choice
public static final int RULE_optionDecl
public static final int RULE_sort_decls
public static final int RULE_one_sort_decl
public static final int RULE_simple_ident_dots
public static final int RULE_simple_ident_dots_comma_list
public static final int RULE_extends_sorts
public static final int RULE_oneof_sorts
public static final int RULE_keyjavatype
public static final int RULE_prog_var_decls
public static final int RULE_string_literal
public static final int RULE_string_value
public static final int RULE_simple_ident
public static final int RULE_simple_ident_comma_list
public static final int RULE_schema_var_decls
public static final int RULE_one_schema_var_decl
public static final int RULE_schema_modifiers
public static final int RULE_one_schema_modal_op_decl
public static final int RULE_pred_decl
public static final int RULE_pred_decls
public static final int RULE_func_decl
public static final int RULE_func_decls
public static final int RULE_arg_sorts_or_formula
public static final int RULE_arg_sorts_or_formula_helper
public static final int RULE_transform_decl
public static final int RULE_transform_decls
public static final int RULE_arrayopid
public static final int RULE_arg_sorts
public static final int RULE_where_to_bind
public static final int RULE_ruleset_decls
public static final int RULE_sortId
public static final int RULE_id_declaration
public static final int RULE_funcpred_name
public static final int RULE_termEOF
public static final int RULE_boolean_literal
public static final int RULE_literals
public static final int RULE_term
public static final int RULE_parallel_term
public static final int RULE_elementary_update_term
public static final int RULE_equivalence_term
public static final int RULE_implication_term
public static final int RULE_disjunction_term
public static final int RULE_conjunction_term
public static final int RULE_term60
public static final int RULE_unary_formula
public static final int RULE_equality_term
public static final int RULE_comparison_term
public static final int RULE_weak_arith_term
public static final int RULE_strong_arith_term_1
public static final int RULE_strong_arith_term_2
public static final int RULE_update_term
public static final int RULE_substitution_term
public static final int RULE_cast_term
public static final int RULE_unary_minus_term
public static final int RULE_atom_prefix
public static final int RULE_bracket_term
public static final int RULE_bracket_suffix_heap
public static final int RULE_brace_suffix
public static final int RULE_primitive_labeled_term
public static final int RULE_termParen
public static final int RULE_abbreviation
public static final int RULE_primitive_term
public static final int RULE_accessterm
public static final int RULE_attribute
public static final int RULE_call
public static final int RULE_label
public static final int RULE_single_label
public static final int RULE_location_term
public static final int RULE_ifThenElseTerm
public static final int RULE_ifExThenElseTerm
public static final int RULE_locset_term
public static final int RULE_bound_variables
public static final int RULE_one_bound_variable
public static final int RULE_argument_list
public static final int RULE_number
public static final int RULE_char_literal
public static final int RULE_varId
public static final int RULE_varIds
public static final int RULE_triggers
public static final int RULE_taclet
public static final int RULE_modifiers
public static final int RULE_seq
public static final int RULE_seqEOF
public static final int RULE_termorseq
public static final int RULE_semisequent
public static final int RULE_varexplist
public static final int RULE_varexp
public static final int RULE_varexpId
public static final int RULE_varexp_argument
public static final int RULE_goalspecs
public static final int RULE_goalspecwithoption
public static final int RULE_option
public static final int RULE_option_list
public static final int RULE_goalspec
public static final int RULE_replacewith
public static final int RULE_add
public static final int RULE_addrules
public static final int RULE_addprogvar
public static final int RULE_tacletlist
public static final int RULE_pvset
public static final int RULE_rulesets
public static final int RULE_ruleset
public static final int RULE_metaId
public static final int RULE_metaTerm
public static final int RULE_contracts
public static final int RULE_invariants
public static final int RULE_one_contract
public static final int RULE_one_invariant
public static final int RULE_rulesOrAxioms
public static final int RULE_bootClassPath
public static final int RULE_classPaths
public static final int RULE_javaSource
public static final int RULE_oneJavaSource
public static final int RULE_profile
public static final int RULE_preferences
public static final int RULE_proofScript
public static final int RULE_proof
public static final java.lang.String[] ruleNames
public static final org.antlr.v4.runtime.Vocabulary VOCABULARY
@Deprecated public static final java.lang.String[] tokenNames
VOCABULARY
instead.public static final java.lang.String _serializedATN
public static final org.antlr.v4.runtime.atn.ATN _ATN
@Deprecated public java.lang.String[] getTokenNames()
getTokenNames
in class org.antlr.v4.runtime.Recognizer<org.antlr.v4.runtime.Token,org.antlr.v4.runtime.atn.ParserATNSimulator>
public org.antlr.v4.runtime.Vocabulary getVocabulary()
getVocabulary
in class org.antlr.v4.runtime.Recognizer<org.antlr.v4.runtime.Token,org.antlr.v4.runtime.atn.ParserATNSimulator>
public java.lang.String getGrammarFileName()
getGrammarFileName
in class org.antlr.v4.runtime.Recognizer<org.antlr.v4.runtime.Token,org.antlr.v4.runtime.atn.ParserATNSimulator>
public java.lang.String[] getRuleNames()
getRuleNames
in class org.antlr.v4.runtime.Recognizer<org.antlr.v4.runtime.Token,org.antlr.v4.runtime.atn.ParserATNSimulator>
public java.lang.String getSerializedATN()
getSerializedATN
in class org.antlr.v4.runtime.Recognizer<org.antlr.v4.runtime.Token,org.antlr.v4.runtime.atn.ParserATNSimulator>
public org.antlr.v4.runtime.atn.ATN getATN()
getATN
in class org.antlr.v4.runtime.Recognizer<org.antlr.v4.runtime.Token,org.antlr.v4.runtime.atn.ParserATNSimulator>
public SyntaxErrorReporter getErrorReporter()
public final KeYParser.FileContext file() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.DeclsContext decls() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.ProblemContext problem() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.One_include_statementContext one_include_statement() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.One_includeContext one_include() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.Options_choiceContext options_choice() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.Activated_choiceContext activated_choice() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.Option_declsContext option_decls() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.ChoiceContext choice() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.OptionDeclContext optionDecl() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.Sort_declsContext sort_decls() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.One_sort_declContext one_sort_decl() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.Simple_ident_dotsContext simple_ident_dots() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.Simple_ident_dots_comma_listContext simple_ident_dots_comma_list() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.Extends_sortsContext extends_sorts() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.Oneof_sortsContext oneof_sorts() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.KeyjavatypeContext keyjavatype() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.Prog_var_declsContext prog_var_decls() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.String_literalContext string_literal() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.String_valueContext string_value() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.Simple_identContext simple_ident() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.Simple_ident_comma_listContext simple_ident_comma_list() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.Schema_var_declsContext schema_var_decls() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.One_schema_var_declContext one_schema_var_decl() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.Schema_modifiersContext schema_modifiers() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.One_schema_modal_op_declContext one_schema_modal_op_decl() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.Pred_declContext pred_decl() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.Pred_declsContext pred_decls() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.Func_declContext func_decl() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.Func_declsContext func_decls() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.Arg_sorts_or_formulaContext arg_sorts_or_formula() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.Arg_sorts_or_formula_helperContext arg_sorts_or_formula_helper() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.Transform_declContext transform_decl() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.Transform_declsContext transform_decls() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.ArrayopidContext arrayopid() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.Arg_sortsContext arg_sorts() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.Where_to_bindContext where_to_bind() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.Ruleset_declsContext ruleset_decls() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.SortIdContext sortId() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.Id_declarationContext id_declaration() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.Funcpred_nameContext funcpred_name() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.TermEOFContext termEOF() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.Boolean_literalContext boolean_literal() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.LiteralsContext literals() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.TermContext term() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.Parallel_termContext parallel_term() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.Elementary_update_termContext elementary_update_term() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.Equivalence_termContext equivalence_term() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.Implication_termContext implication_term() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.Disjunction_termContext disjunction_term() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.Conjunction_termContext conjunction_term() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.Term60Context term60() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.Unary_formulaContext unary_formula() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.Equality_termContext equality_term() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.Comparison_termContext comparison_term() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.Weak_arith_termContext weak_arith_term() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.Strong_arith_term_1Context strong_arith_term_1() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.Strong_arith_term_2Context strong_arith_term_2() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.Update_termContext update_term() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.Substitution_termContext substitution_term() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.Cast_termContext cast_term() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.Unary_minus_termContext unary_minus_term() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.Atom_prefixContext atom_prefix() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.Bracket_termContext bracket_term() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.Bracket_suffix_heapContext bracket_suffix_heap() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.Brace_suffixContext brace_suffix() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.Primitive_labeled_termContext primitive_labeled_term() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.TermParenContext termParen() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.AbbreviationContext abbreviation() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.Primitive_termContext primitive_term() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.AccesstermContext accessterm() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.AttributeContext attribute() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.CallContext call() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.LabelContext label() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.Single_labelContext single_label() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.Location_termContext location_term() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.IfThenElseTermContext ifThenElseTerm() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.IfExThenElseTermContext ifExThenElseTerm() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.Locset_termContext locset_term() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.Bound_variablesContext bound_variables() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.One_bound_variableContext one_bound_variable() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.Argument_listContext argument_list() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.NumberContext number() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.Char_literalContext char_literal() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.VarIdContext varId() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.VarIdsContext varIds() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.TriggersContext triggers() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.TacletContext taclet() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.ModifiersContext modifiers() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.SeqContext seq() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.SeqEOFContext seqEOF() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.TermorseqContext termorseq() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.SemisequentContext semisequent() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.VarexplistContext varexplist() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.VarexpContext varexp() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.VarexpIdContext varexpId() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.Varexp_argumentContext varexp_argument() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.GoalspecsContext goalspecs() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.GoalspecwithoptionContext goalspecwithoption() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.OptionContext option() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.Option_listContext option_list() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.GoalspecContext goalspec() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.ReplacewithContext replacewith() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.AddContext add() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.AddrulesContext addrules() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.AddprogvarContext addprogvar() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.TacletlistContext tacletlist() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.PvsetContext pvset() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.RulesetsContext rulesets() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.RulesetContext ruleset() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.MetaIdContext metaId() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.MetaTermContext metaTerm() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.ContractsContext contracts() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.InvariantsContext invariants() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.One_contractContext one_contract() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.One_invariantContext one_invariant() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.RulesOrAxiomsContext rulesOrAxioms() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.BootClassPathContext bootClassPath() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.ClassPathsContext classPaths() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.JavaSourceContext javaSource() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.OneJavaSourceContext oneJavaSource() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.ProfileContext profile() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.PreferencesContext preferences() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.ProofScriptContext proofScript() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
public final KeYParser.ProofContext proof() throws org.antlr.v4.runtime.RecognitionException
org.antlr.v4.runtime.RecognitionException
Copyright © 2003-2019 The KeY-Project.