public class KeYJMLPreParser
extends org.antlr.runtime.Parser
Modifier and Type | Class and Description |
---|---|
protected class |
KeYJMLPreParser.DFA1 |
protected class |
KeYJMLPreParser.DFA15 |
protected class |
KeYJMLPreParser.DFA18 |
protected class |
KeYJMLPreParser.DFA2 |
protected class |
KeYJMLPreParser.DFA23 |
protected class |
KeYJMLPreParser.DFA3 |
protected class |
KeYJMLPreParser.DFA39 |
protected class |
KeYJMLPreParser.DFA43 |
protected class |
KeYJMLPreParser.DFA5 |
protected class |
KeYJMLPreParser.DFA9 |
Modifier and Type | Field and Description |
---|---|
static int |
ABSTRACT |
static int |
ACCESSIBLE |
static int |
ACCESSIBLE_REDUNDANTLY |
static int |
ALSO |
static int |
ASSERT |
static int |
ASSERT_REDUNDANTLY |
static int |
ASSIGNABLE |
static int |
ASSIGNABLE_RED |
static int |
ASSIGNS |
static int |
ASSIGNS_RED |
static int |
ASSUME |
static int |
ASSUME_REDUNDANTLY |
static int |
AXIOM |
static int |
AXIOM_NAME_BEGIN |
static int |
AXIOM_NAME_END |
static int |
AXION_NAME_END |
static int |
BEHAVIOR |
static int |
BEHAVIOUR |
static int |
BODY |
static int |
BRACE_DISPATCH |
static int |
BREAK_BEHAVIOR |
static int |
BREAK_BEHAVIOUR |
static int |
BREAKS |
static int |
CAPTURES |
static int |
CAPTURES_RED |
static int |
CHAR_LITERAL |
static int |
CODE |
static int |
CODE_BIGINT_MATH |
static int |
CODE_JAVA_MATH |
static int |
CODE_SAFE_MATH |
static int |
CODE_SAVE_MATH |
static int |
COMMA |
static int |
CONST |
static int |
CONSTRAINT |
static int |
CONSTRAINT_RED |
static int |
CONTINUE_BEHAVIOR |
static int |
CONTINUE_BEHAVIOUR |
static int |
CONTINUES |
static int |
DEBUG |
static int |
DECIMALINTEGERLITERAL |
static int |
DECREASES |
static int |
DECREASES_REDUNDANTLY |
static int |
DECREASING |
static int |
DECREASING_REDUNDANTLY |
static int |
DETERMINES |
protected KeYJMLPreParser.DFA1 |
dfa1 |
(package private) static short[] |
DFA1_accept |
(package private) static java.lang.String |
DFA1_acceptS |
(package private) static short[] |
DFA1_eof |
(package private) static java.lang.String |
DFA1_eofS |
(package private) static short[] |
DFA1_eot |
(package private) static java.lang.String |
DFA1_eotS |
(package private) static char[] |
DFA1_max |
(package private) static java.lang.String |
DFA1_maxS |
(package private) static char[] |
DFA1_min |
(package private) static java.lang.String |
DFA1_minS |
(package private) static short[] |
DFA1_special |
(package private) static java.lang.String |
DFA1_specialS |
(package private) static short[][] |
DFA1_transition |
(package private) static java.lang.String[] |
DFA1_transitionS |
protected KeYJMLPreParser.DFA15 |
dfa15 |
(package private) static short[] |
DFA15_accept |
(package private) static java.lang.String |
DFA15_acceptS |
(package private) static short[] |
DFA15_eof |
(package private) static java.lang.String |
DFA15_eofS |
(package private) static short[] |
DFA15_eot |
(package private) static java.lang.String |
DFA15_eotS |
(package private) static char[] |
DFA15_max |
(package private) static java.lang.String |
DFA15_maxS |
(package private) static char[] |
DFA15_min |
(package private) static java.lang.String |
DFA15_minS |
(package private) static short[] |
DFA15_special |
(package private) static java.lang.String |
DFA15_specialS |
(package private) static short[][] |
DFA15_transition |
(package private) static java.lang.String[] |
DFA15_transitionS |
protected KeYJMLPreParser.DFA18 |
dfa18 |
(package private) static short[] |
DFA18_accept |
(package private) static java.lang.String |
DFA18_acceptS |
(package private) static short[] |
DFA18_eof |
(package private) static java.lang.String |
DFA18_eofS |
(package private) static short[] |
DFA18_eot |
(package private) static java.lang.String |
DFA18_eotS |
(package private) static char[] |
DFA18_max |
(package private) static java.lang.String |
DFA18_maxS |
(package private) static char[] |
DFA18_min |
(package private) static java.lang.String |
DFA18_minS |
(package private) static short[] |
DFA18_special |
(package private) static java.lang.String |
DFA18_specialS |
(package private) static short[][] |
DFA18_transition |
(package private) static java.lang.String[] |
DFA18_transitionS |
protected KeYJMLPreParser.DFA2 |
dfa2 |
(package private) static short[] |
DFA2_accept |
(package private) static java.lang.String |
DFA2_acceptS |
(package private) static short[] |
DFA2_eof |
(package private) static java.lang.String |
DFA2_eofS |
(package private) static short[] |
DFA2_eot |
(package private) static java.lang.String |
DFA2_eotS |
(package private) static char[] |
DFA2_max |
(package private) static java.lang.String |
DFA2_maxS |
(package private) static char[] |
DFA2_min |
(package private) static java.lang.String |
DFA2_minS |
(package private) static short[] |
DFA2_special |
(package private) static java.lang.String |
DFA2_specialS |
(package private) static short[][] |
DFA2_transition |
(package private) static java.lang.String[] |
DFA2_transitionS |
protected KeYJMLPreParser.DFA23 |
dfa23 |
(package private) static short[] |
DFA23_accept |
(package private) static java.lang.String |
DFA23_acceptS |
(package private) static short[] |
DFA23_eof |
(package private) static java.lang.String |
DFA23_eofS |
(package private) static short[] |
DFA23_eot |
(package private) static java.lang.String |
DFA23_eotS |
(package private) static char[] |
DFA23_max |
(package private) static java.lang.String |
DFA23_maxS |
(package private) static char[] |
DFA23_min |
(package private) static java.lang.String |
DFA23_minS |
(package private) static short[] |
DFA23_special |
(package private) static java.lang.String |
DFA23_specialS |
(package private) static short[][] |
DFA23_transition |
(package private) static java.lang.String[] |
DFA23_transitionS |
protected KeYJMLPreParser.DFA3 |
dfa3 |
(package private) static short[] |
DFA3_accept |
(package private) static java.lang.String |
DFA3_acceptS |
(package private) static short[] |
DFA3_eof |
(package private) static java.lang.String |
DFA3_eofS |
(package private) static short[] |
DFA3_eot |
(package private) static java.lang.String |
DFA3_eotS |
(package private) static char[] |
DFA3_max |
(package private) static java.lang.String |
DFA3_maxS |
(package private) static char[] |
DFA3_min |
(package private) static java.lang.String |
DFA3_minS |
(package private) static short[] |
DFA3_special |
(package private) static java.lang.String |
DFA3_specialS |
(package private) static short[][] |
DFA3_transition |
(package private) static java.lang.String[] |
DFA3_transitionS |
protected KeYJMLPreParser.DFA39 |
dfa39 |
(package private) static short[] |
DFA39_accept |
(package private) static java.lang.String |
DFA39_acceptS |
(package private) static short[] |
DFA39_eof |
(package private) static java.lang.String |
DFA39_eofS |
(package private) static short[] |
DFA39_eot |
(package private) static java.lang.String |
DFA39_eotS |
(package private) static char[] |
DFA39_max |
(package private) static java.lang.String |
DFA39_maxS |
(package private) static char[] |
DFA39_min |
(package private) static java.lang.String |
DFA39_minS |
(package private) static short[] |
DFA39_special |
(package private) static java.lang.String |
DFA39_specialS |
(package private) static short[][] |
DFA39_transition |
(package private) static java.lang.String[] |
DFA39_transitionS |
protected KeYJMLPreParser.DFA43 |
dfa43 |
(package private) static short[] |
DFA43_accept |
(package private) static java.lang.String |
DFA43_acceptS |
(package private) static short[] |
DFA43_eof |
(package private) static java.lang.String |
DFA43_eofS |
(package private) static short[] |
DFA43_eot |
(package private) static java.lang.String |
DFA43_eotS |
(package private) static char[] |
DFA43_max |
(package private) static java.lang.String |
DFA43_maxS |
(package private) static char[] |
DFA43_min |
(package private) static java.lang.String |
DFA43_minS |
(package private) static short[] |
DFA43_special |
(package private) static java.lang.String |
DFA43_specialS |
(package private) static short[][] |
DFA43_transition |
(package private) static java.lang.String[] |
DFA43_transitionS |
protected KeYJMLPreParser.DFA5 |
dfa5 |
(package private) static short[] |
DFA5_accept |
(package private) static java.lang.String |
DFA5_acceptS |
(package private) static short[] |
DFA5_eof |
(package private) static java.lang.String |
DFA5_eofS |
(package private) static short[] |
DFA5_eot |
(package private) static java.lang.String |
DFA5_eotS |
(package private) static char[] |
DFA5_max |
(package private) static java.lang.String |
DFA5_maxS |
(package private) static char[] |
DFA5_min |
(package private) static java.lang.String |
DFA5_minS |
(package private) static short[] |
DFA5_special |
(package private) static java.lang.String |
DFA5_specialS |
(package private) static short[][] |
DFA5_transition |
(package private) static java.lang.String[] |
DFA5_transitionS |
protected KeYJMLPreParser.DFA9 |
dfa9 |
(package private) static short[] |
DFA9_accept |
(package private) static java.lang.String |
DFA9_acceptS |
(package private) static short[] |
DFA9_eof |
(package private) static java.lang.String |
DFA9_eofS |
(package private) static short[] |
DFA9_eot |
(package private) static java.lang.String |
DFA9_eotS |
(package private) static char[] |
DFA9_max |
(package private) static java.lang.String |
DFA9_maxS |
(package private) static char[] |
DFA9_min |
(package private) static java.lang.String |
DFA9_minS |
(package private) static short[] |
DFA9_special |
(package private) static java.lang.String |
DFA9_specialS |
(package private) static short[][] |
DFA9_transition |
(package private) static java.lang.String[] |
DFA9_transitionS |
static int |
DIGIT |
static int |
DIGITS |
static int |
DIVERGES |
static int |
DIVERGES_RED |
static int |
DOT |
static int |
DURATION |
static int |
DURATION_RED |
static int |
EMPTYBRACKETS |
static int |
ENSURES |
static int |
ENSURES_FREE |
static int |
ENSURES_RED |
static int |
EOF |
static int |
EQUALITY |
static int |
ESC |
static int |
EXCEPTIONAL_BEHAVIOR |
static int |
EXCEPTIONAL_BEHAVIOUR |
private SLTranslationExceptionManager |
excManager |
static int |
EXSURES |
static int |
EXSURES_RED |
static int |
FINAL |
static org.antlr.runtime.BitSet |
FOLLOW_ABSTRACT_in_modifier707 |
static org.antlr.runtime.BitSet |
FOLLOW_accessible_clause_in_simple_spec_body_clause2846 |
static org.antlr.runtime.BitSet |
FOLLOW_accessible_keyword_in_accessible_clause3409 |
static org.antlr.runtime.BitSet |
FOLLOW_accessible_keyword_in_depends_clause4872 |
static org.antlr.runtime.BitSet |
FOLLOW_accessible_keyword_in_synpred1_KeYJMLPreParser216 |
static org.antlr.runtime.BitSet |
FOLLOW_also_keyword_in_block_loop_specification6259 |
static org.antlr.runtime.BitSet |
FOLLOW_also_keyword_in_generic_spec_case_seq2709 |
static org.antlr.runtime.BitSet |
FOLLOW_also_keyword_in_method_specification1560 |
static org.antlr.runtime.BitSet |
FOLLOW_also_keyword_in_method_specification1596 |
static org.antlr.runtime.BitSet |
FOLLOW_assert_keyword_in_assert_statement6318 |
static org.antlr.runtime.BitSet |
FOLLOW_assert_statement_in_classlevel_element385 |
static org.antlr.runtime.BitSet |
FOLLOW_assert_statement_in_methodlevel_element559 |
static org.antlr.runtime.BitSet |
FOLLOW_assignable_clause_in_loop_specification5556 |
static org.antlr.runtime.BitSet |
FOLLOW_assignable_clause_in_simple_spec_body_clause2831 |
static org.antlr.runtime.BitSet |
FOLLOW_assignable_keyword_in_assignable_clause3288 |
static org.antlr.runtime.BitSet |
FOLLOW_assume_keyword_in_assume_statement5917 |
static org.antlr.runtime.BitSet |
FOLLOW_assume_statement_in_classlevel_element399 |
static org.antlr.runtime.BitSet |
FOLLOW_assume_statement_in_methodlevel_element572 |
static org.antlr.runtime.BitSet |
FOLLOW_AXIOM_in_class_axiom1442 |
static org.antlr.runtime.BitSet |
FOLLOW_AXIOM_NAME_BEGIN_in_axiom_name1346 |
static org.antlr.runtime.BitSet |
FOLLOW_AXIOM_NAME_BEGIN_in_param_decl4687 |
static org.antlr.runtime.BitSet |
FOLLOW_AXIOM_NAME_END_in_axiom_name1352 |
static org.antlr.runtime.BitSet |
FOLLOW_AXION_NAME_END_in_param_decl4702 |
static org.antlr.runtime.BitSet |
FOLLOW_behavior_keyword_in_behavior_spec_case1909 |
static org.antlr.runtime.BitSet |
FOLLOW_behavior_spec_case_in_heavyweight_spec_case1795 |
static org.antlr.runtime.BitSet |
FOLLOW_block_loop_specification_in_methodlevel_element624 |
static org.antlr.runtime.BitSet |
FOLLOW_block_specification_in_methodlevel_element611 |
static org.antlr.runtime.BitSet |
FOLLOW_BODY_in_merge_point_statement5344 |
static org.antlr.runtime.BitSet |
FOLLOW_BODY_in_method_declaration4345 |
static org.antlr.runtime.BitSet |
FOLLOW_break_behavior_keyword_in_break_behavior_spec_case6545 |
static org.antlr.runtime.BitSet |
FOLLOW_break_behavior_spec_case_in_heavyweight_spec_case1809 |
static org.antlr.runtime.BitSet |
FOLLOW_breaks_clause_in_simple_spec_body_clause3019 |
static org.antlr.runtime.BitSet |
FOLLOW_BREAKS_in_breaks_keyword6414 |
static org.antlr.runtime.BitSet |
FOLLOW_breaks_keyword_in_breaks_clause6397 |
static org.antlr.runtime.BitSet |
FOLLOW_captures_clause_in_simple_spec_body_clause2989 |
static org.antlr.runtime.BitSet |
FOLLOW_captures_keyword_in_captures_clause3834 |
static org.antlr.runtime.BitSet |
FOLLOW_class_axiom_in_classlevel_element303 |
static org.antlr.runtime.BitSet |
FOLLOW_class_invariant_in_classlevel_element204 |
static org.antlr.runtime.BitSet |
FOLLOW_classlevel_element_in_classlevel_comment131 |
static org.antlr.runtime.BitSet |
FOLLOW_CODE_BIGINT_MATH_in_modifier1268 |
static org.antlr.runtime.BitSet |
FOLLOW_CODE_JAVA_MATH_in_modifier1230 |
static org.antlr.runtime.BitSet |
FOLLOW_CODE_SAVE_MATH_in_modifier1249 |
static org.antlr.runtime.BitSet |
FOLLOW_COMMA_in_param_list4475 |
static org.antlr.runtime.BitSet |
FOLLOW_constraint_keyword_in_history_constraint4912 |
static org.antlr.runtime.BitSet |
FOLLOW_continue_behavior_keyword_in_continue_behavior_spec_case6608 |
static org.antlr.runtime.BitSet |
FOLLOW_continue_behavior_spec_case_in_heavyweight_spec_case1823 |
static org.antlr.runtime.BitSet |
FOLLOW_continues_clause_in_simple_spec_body_clause3038 |
static org.antlr.runtime.BitSet |
FOLLOW_CONTINUES_in_continues_keyword6462 |
static org.antlr.runtime.BitSet |
FOLLOW_continues_keyword_in_continues_clause6445 |
static org.antlr.runtime.BitSet |
FOLLOW_datagroup_clause_in_classlevel_element355 |
static org.antlr.runtime.BitSet |
FOLLOW_DEBUG_in_debug_statement5244 |
static org.antlr.runtime.BitSet |
FOLLOW_debug_statement_in_methodlevel_element598 |
static org.antlr.runtime.BitSet |
FOLLOW_decreasing_keyword_in_variant_function5731 |
static org.antlr.runtime.BitSet |
FOLLOW_depends_clause_in_classlevel_element225 |
static org.antlr.runtime.BitSet |
FOLLOW_determines_clause_in_simple_spec_body_clause3102 |
static org.antlr.runtime.BitSet |
FOLLOW_DETERMINES_in_determines_keyword3254 |
static org.antlr.runtime.BitSet |
FOLLOW_determines_keyword_in_determines_clause3230 |
static org.antlr.runtime.BitSet |
FOLLOW_determines_keyword_in_loop_determines_clause5880 |
static org.antlr.runtime.BitSet |
FOLLOW_diverges_clause_in_simple_spec_body_clause2923 |
static org.antlr.runtime.BitSet |
FOLLOW_diverges_keyword_in_diverges_clause3791 |
static org.antlr.runtime.BitSet |
FOLLOW_duration_clause_in_simple_spec_body_clause3010 |
static org.antlr.runtime.BitSet |
FOLLOW_duration_keyword_in_duration_clause4019 |
static org.antlr.runtime.BitSet |
FOLLOW_EMPTYBRACKETS_in_field_declaration4246 |
static org.antlr.runtime.BitSet |
FOLLOW_EMPTYBRACKETS_in_param_decl4717 |
static org.antlr.runtime.BitSet |
FOLLOW_EMPTYBRACKETS_in_type4132 |
static org.antlr.runtime.BitSet |
FOLLOW_ensures_clause_in_simple_spec_body_clause2861 |
static org.antlr.runtime.BitSet |
FOLLOW_ensures_free_clause_in_simple_spec_body_clause2879 |
static org.antlr.runtime.BitSet |
FOLLOW_ENSURES_FREE_in_ensures_free_clause3609 |
static org.antlr.runtime.BitSet |
FOLLOW_ensures_keyword_in_ensures_clause3546 |
static org.antlr.runtime.BitSet |
FOLLOW_EOF_in_classlevel_comment163 |
static org.antlr.runtime.BitSet |
FOLLOW_EOF_in_methodlevel_comment466 |
static org.antlr.runtime.BitSet |
FOLLOW_EQUALITY_in_initialiser6136 |
static org.antlr.runtime.BitSet |
FOLLOW_exceptional_behavior_keyword_in_exceptional_behavior_spec_case2103 |
static org.antlr.runtime.BitSet |
FOLLOW_exceptional_behavior_spec_case_in_heavyweight_spec_case1837 |
static org.antlr.runtime.BitSet |
FOLLOW_expression_in_accessible_clause3413 |
static org.antlr.runtime.BitSet |
FOLLOW_expression_in_assert_statement6322 |
static org.antlr.runtime.BitSet |
FOLLOW_expression_in_assignable_clause3292 |
static org.antlr.runtime.BitSet |
FOLLOW_expression_in_assume_statement5921 |
static org.antlr.runtime.BitSet |
FOLLOW_expression_in_breaks_clause6401 |
static org.antlr.runtime.BitSet |
FOLLOW_expression_in_captures_clause3838 |
static org.antlr.runtime.BitSet |
FOLLOW_expression_in_class_axiom1446 |
static org.antlr.runtime.BitSet |
FOLLOW_expression_in_class_invariant1317 |
static org.antlr.runtime.BitSet |
FOLLOW_expression_in_continues_clause6449 |
static org.antlr.runtime.BitSet |
FOLLOW_expression_in_debug_statement5248 |
static org.antlr.runtime.BitSet |
FOLLOW_expression_in_depends_clause4876 |
static org.antlr.runtime.BitSet |
FOLLOW_expression_in_determines_clause3234 |
static org.antlr.runtime.BitSet |
FOLLOW_expression_in_diverges_clause3795 |
static org.antlr.runtime.BitSet |
FOLLOW_expression_in_duration_clause4023 |
static org.antlr.runtime.BitSet |
FOLLOW_expression_in_ensures_clause3550 |
static org.antlr.runtime.BitSet |
FOLLOW_expression_in_ensures_free_clause3613 |
static org.antlr.runtime.BitSet |
FOLLOW_expression_in_history_constraint4916 |
static org.antlr.runtime.BitSet |
FOLLOW_expression_in_in_group_clause5108 |
static org.antlr.runtime.BitSet |
FOLLOW_expression_in_initialiser6140 |
static org.antlr.runtime.BitSet |
FOLLOW_expression_in_initially_clause1515 |
static org.antlr.runtime.BitSet |
FOLLOW_expression_in_loop_determines_clause5884 |
static org.antlr.runtime.BitSet |
FOLLOW_expression_in_loop_invariant_free5654 |
static org.antlr.runtime.BitSet |
FOLLOW_expression_in_loop_invariant5622 |
static org.antlr.runtime.BitSet |
FOLLOW_expression_in_loop_separates_clause5844 |
static org.antlr.runtime.BitSet |
FOLLOW_expression_in_maps_into_clause5156 |
static org.antlr.runtime.BitSet |
FOLLOW_expression_in_measured_by_clause3482 |
static org.antlr.runtime.BitSet |
FOLLOW_expression_in_monitors_for_clause4980 |
static org.antlr.runtime.BitSet |
FOLLOW_expression_in_nowarn_pragma5211 |
static org.antlr.runtime.BitSet |
FOLLOW_expression_in_readable_if_clause5015 |
static org.antlr.runtime.BitSet |
FOLLOW_expression_in_represents_clause4808 |
static org.antlr.runtime.BitSet |
FOLLOW_expression_in_requires_clause2500 |
static org.antlr.runtime.BitSet |
FOLLOW_expression_in_requires_free_clause2571 |
static org.antlr.runtime.BitSet |
FOLLOW_expression_in_returns_clause6497 |
static org.antlr.runtime.BitSet |
FOLLOW_expression_in_separates_clause3166 |
static org.antlr.runtime.BitSet |
FOLLOW_expression_in_set_statement5282 |
static org.antlr.runtime.BitSet |
FOLLOW_expression_in_signals_clause3653 |
static org.antlr.runtime.BitSet |
FOLLOW_expression_in_signals_only_clause3734 |
static org.antlr.runtime.BitSet |
FOLLOW_expression_in_spec_var_decls2341 |
static org.antlr.runtime.BitSet |
FOLLOW_expression_in_synpred1_KeYJMLPreParser218 |
static org.antlr.runtime.BitSet |
FOLLOW_expression_in_variant_function5735 |
static org.antlr.runtime.BitSet |
FOLLOW_expression_in_when_clause3925 |
static org.antlr.runtime.BitSet |
FOLLOW_expression_in_working_space_clause3974 |
static org.antlr.runtime.BitSet |
FOLLOW_expression_in_writable_if_clause5050 |
static org.antlr.runtime.BitSet |
FOLLOW_field_declaration_in_field_or_method_declaration4204 |
static org.antlr.runtime.BitSet |
FOLLOW_field_or_method_declaration_in_classlevel_element251 |
static org.antlr.runtime.BitSet |
FOLLOW_field_or_method_declaration_in_methodlevel_element507 |
static org.antlr.runtime.BitSet |
FOLLOW_FINAL_in_modifier732 |
static org.antlr.runtime.BitSet |
FOLLOW_FORALL_in_spec_var_decls2337 |
static org.antlr.runtime.BitSet |
FOLLOW_free_spec_header_in_generic_spec_case2197 |
static org.antlr.runtime.BitSet |
FOLLOW_generic_spec_body_in_generic_spec_case2230 |
static org.antlr.runtime.BitSet |
FOLLOW_generic_spec_body_in_generic_spec_case2256 |
static org.antlr.runtime.BitSet |
FOLLOW_generic_spec_case_in_behavior_spec_case1917 |
static org.antlr.runtime.BitSet |
FOLLOW_generic_spec_case_in_break_behavior_spec_case6553 |
static org.antlr.runtime.BitSet |
FOLLOW_generic_spec_case_in_continue_behavior_spec_case6616 |
static org.antlr.runtime.BitSet |
FOLLOW_generic_spec_case_in_exceptional_behavior_spec_case2111 |
static org.antlr.runtime.BitSet |
FOLLOW_generic_spec_case_in_generic_spec_case_seq2691 |
static org.antlr.runtime.BitSet |
FOLLOW_generic_spec_case_in_generic_spec_case_seq2723 |
static org.antlr.runtime.BitSet |
FOLLOW_generic_spec_case_in_lightweight_spec_case1731 |
static org.antlr.runtime.BitSet |
FOLLOW_generic_spec_case_in_model_behavior_spec_case2044 |
static org.antlr.runtime.BitSet |
FOLLOW_generic_spec_case_in_normal_behavior_spec_case1981 |
static org.antlr.runtime.BitSet |
FOLLOW_generic_spec_case_in_return_behavior_spec_case6679 |
static org.antlr.runtime.BitSet |
FOLLOW_generic_spec_case_seq_in_generic_spec_body2640 |
static org.antlr.runtime.BitSet |
FOLLOW_GHOST_in_modifier760 |
static org.antlr.runtime.BitSet |
FOLLOW_heavyweight_spec_case_in_spec_case1688 |
static org.antlr.runtime.BitSet |
FOLLOW_HELPER_in_modifier788 |
static org.antlr.runtime.BitSet |
FOLLOW_history_constraint_in_classlevel_element277 |
static org.antlr.runtime.BitSet |
FOLLOW_IDENT_in_axiom_name1350 |
static org.antlr.runtime.BitSet |
FOLLOW_IDENT_in_field_or_method_declaration4162 |
static org.antlr.runtime.BitSet |
FOLLOW_IDENT_in_old_clause4084 |
static org.antlr.runtime.BitSet |
FOLLOW_IDENT_in_param_decl4653 |
static org.antlr.runtime.BitSet |
FOLLOW_IDENT_in_param_decl4760 |
static org.antlr.runtime.BitSet |
FOLLOW_IDENT_in_type4121 |
static org.antlr.runtime.BitSet |
FOLLOW_in_group_clause_in_datagroup_clause5081 |
static org.antlr.runtime.BitSet |
FOLLOW_in_keyword_in_in_group_clause5104 |
static org.antlr.runtime.BitSet |
FOLLOW_initialiser_in_field_declaration4265 |
static org.antlr.runtime.BitSet |
FOLLOW_INITIALISER_in_old_clause4089 |
static org.antlr.runtime.BitSet |
FOLLOW_initially_clause_in_classlevel_element290 |
static org.antlr.runtime.BitSet |
FOLLOW_INITIALLY_in_initially_clause1511 |
static org.antlr.runtime.BitSet |
FOLLOW_INSTANCE_in_modifier815 |
static org.antlr.runtime.BitSet |
FOLLOW_invariant_keyword_in_class_invariant1308 |
static org.antlr.runtime.BitSet |
FOLLOW_lightweight_spec_case_in_spec_case1676 |
static org.antlr.runtime.BitSet |
FOLLOW_LOOP_CONTRACT_in_loop_contract_keyword6294 |
static org.antlr.runtime.BitSet |
FOLLOW_loop_contract_keyword_in_block_loop_specification6229 |
static org.antlr.runtime.BitSet |
FOLLOW_loop_contract_keyword_in_block_loop_specification6263 |
static org.antlr.runtime.BitSet |
FOLLOW_loop_determines_clause_in_loop_specification5533 |
static org.antlr.runtime.BitSet |
FOLLOW_LOOP_INVARIANT_FREE_in_loop_invariant_free5650 |
static org.antlr.runtime.BitSet |
FOLLOW_loop_invariant_free_in_loop_specification5416 |
static org.antlr.runtime.BitSet |
FOLLOW_loop_invariant_free_in_loop_specification5486 |
static org.antlr.runtime.BitSet |
FOLLOW_loop_invariant_in_loop_specification5397 |
static org.antlr.runtime.BitSet |
FOLLOW_loop_invariant_in_loop_specification5462 |
static org.antlr.runtime.BitSet |
FOLLOW_loop_separates_clause_in_loop_specification5510 |
static org.antlr.runtime.BitSet |
FOLLOW_loop_specification_in_methodlevel_element546 |
static org.antlr.runtime.BitSet |
FOLLOW_LPAREN_in_expression6001 |
static org.antlr.runtime.BitSet |
FOLLOW_LPAREN_in_param_list4411 |
static org.antlr.runtime.BitSet |
FOLLOW_LPAREN_in_synpred2_KeYJMLPreParser4172 |
static org.antlr.runtime.BitSet |
FOLLOW_maintaining_keyword_in_loop_invariant5618 |
static org.antlr.runtime.BitSet |
FOLLOW_maps_into_clause_in_datagroup_clause5085 |
static org.antlr.runtime.BitSet |
FOLLOW_maps_keyword_in_maps_into_clause5152 |
static org.antlr.runtime.BitSet |
FOLLOW_measured_by_clause_in_simple_spec_body_clause2940 |
static org.antlr.runtime.BitSet |
FOLLOW_measured_by_keyword_in_measured_by_clause3478 |
static org.antlr.runtime.BitSet |
FOLLOW_MERGE_PARAMS_in_merge_point_statement5337 |
static org.antlr.runtime.BitSet |
FOLLOW_MERGE_POINT_in_merge_point_statement5311 |
static org.antlr.runtime.BitSet |
FOLLOW_merge_point_statement_in_methodlevel_element533 |
static org.antlr.runtime.BitSet |
FOLLOW_MERGE_PROC_in_merge_point_statement5318 |
static org.antlr.runtime.BitSet |
FOLLOW_method_declaration_in_field_or_method_declaration4181 |
static org.antlr.runtime.BitSet |
FOLLOW_method_specification_in_block_specification6188 |
static org.antlr.runtime.BitSet |
FOLLOW_method_specification_in_classlevel_element238 |
static org.antlr.runtime.BitSet |
FOLLOW_methodlevel_element_in_methodlevel_comment453 |
static org.antlr.runtime.BitSet |
FOLLOW_model_behavior_keyword_in_model_behavior_spec_case2036 |
static org.antlr.runtime.BitSet |
FOLLOW_model_behavior_spec_case_in_heavyweight_spec_case1857 |
static org.antlr.runtime.BitSet |
FOLLOW_MODEL_in_modifier840 |
static org.antlr.runtime.BitSet |
FOLLOW_modifier_in_heavyweight_spec_case1775 |
static org.antlr.runtime.BitSet |
FOLLOW_modifier_in_modifiers674 |
static org.antlr.runtime.BitSet |
FOLLOW_modifiers_in_classlevel_comment115 |
static org.antlr.runtime.BitSet |
FOLLOW_modifiers_in_classlevel_comment150 |
static org.antlr.runtime.BitSet |
FOLLOW_modifiers_in_methodlevel_comment448 |
static org.antlr.runtime.BitSet |
FOLLOW_modifiers_in_old_clause4074 |
static org.antlr.runtime.BitSet |
FOLLOW_monitors_for_clause_in_classlevel_element316 |
static org.antlr.runtime.BitSet |
FOLLOW_MONITORS_FOR_in_monitors_for_clause4976 |
static org.antlr.runtime.BitSet |
FOLLOW_name_clause_in_simple_spec_body_clause2970 |
static org.antlr.runtime.BitSet |
FOLLOW_NEST_END_in_generic_spec_body2648 |
static org.antlr.runtime.BitSet |
FOLLOW_NEST_START_in_generic_spec_body2631 |
static org.antlr.runtime.BitSet |
FOLLOW_NO_STATE_in_modifier1150 |
static org.antlr.runtime.BitSet |
FOLLOW_NON_NULL_in_modifier868 |
static org.antlr.runtime.BitSet |
FOLLOW_normal_behavior_keyword_in_normal_behavior_spec_case1973 |
static org.antlr.runtime.BitSet |
FOLLOW_normal_behavior_spec_case_in_heavyweight_spec_case1847 |
static org.antlr.runtime.BitSet |
FOLLOW_NOWARN_in_nowarn_pragma5207 |
static org.antlr.runtime.BitSet |
FOLLOW_nowarn_pragma_in_classlevel_element413 |
static org.antlr.runtime.BitSet |
FOLLOW_nowarn_pragma_in_methodlevel_element585 |
static org.antlr.runtime.BitSet |
FOLLOW_NULLABLE_BY_DEFAULT_in_modifier918 |
static org.antlr.runtime.BitSet |
FOLLOW_NULLABLE_in_modifier893 |
static org.antlr.runtime.BitSet |
FOLLOW_old_clause_in_spec_var_decls2302 |
static org.antlr.runtime.BitSet |
FOLLOW_OLD_in_old_clause4070 |
static org.antlr.runtime.BitSet |
FOLLOW_param_decl_in_param_list4439 |
static org.antlr.runtime.BitSet |
FOLLOW_param_decl_in_param_list4495 |
static org.antlr.runtime.BitSet |
FOLLOW_param_list_in_method_declaration4326 |
static org.antlr.runtime.BitSet |
FOLLOW_PRIVATE_in_modifier932 |
static org.antlr.runtime.BitSet |
FOLLOW_PROTECTED_in_modifier958 |
static org.antlr.runtime.BitSet |
FOLLOW_PUBLIC_in_modifier982 |
static org.antlr.runtime.BitSet |
FOLLOW_PURE_in_modifier1009 |
static org.antlr.runtime.BitSet |
FOLLOW_readable_if_clause_in_classlevel_element329 |
static org.antlr.runtime.BitSet |
FOLLOW_READABLE_in_readable_if_clause5011 |
static org.antlr.runtime.BitSet |
FOLLOW_represents_clause_in_classlevel_element264 |
static org.antlr.runtime.BitSet |
FOLLOW_represents_keyword_in_represents_clause4804 |
static org.antlr.runtime.BitSet |
FOLLOW_requires_clause_in_spec_header2398 |
static org.antlr.runtime.BitSet |
FOLLOW_requires_free_clause_in_free_spec_header2452 |
static org.antlr.runtime.BitSet |
FOLLOW_REQUIRES_FREE_in_requires_free_clause2567 |
static org.antlr.runtime.BitSet |
FOLLOW_requires_keyword_in_requires_clause2496 |
static org.antlr.runtime.BitSet |
FOLLOW_return_behavior_keyword_in_return_behavior_spec_case6671 |
static org.antlr.runtime.BitSet |
FOLLOW_return_behavior_spec_case_in_heavyweight_spec_case1867 |
static org.antlr.runtime.BitSet |
FOLLOW_returns_clause_in_simple_spec_body_clause3054 |
static org.antlr.runtime.BitSet |
FOLLOW_RETURNS_in_returns_keyword6510 |
static org.antlr.runtime.BitSet |
FOLLOW_returns_keyword_in_returns_clause6493 |
static org.antlr.runtime.BitSet |
FOLLOW_RPAREN_in_expression6019 |
static org.antlr.runtime.BitSet |
FOLLOW_RPAREN_in_param_list4551 |
static org.antlr.runtime.BitSet |
FOLLOW_SEMICOLON_in_assert_statement6342 |
static org.antlr.runtime.BitSet |
FOLLOW_SEMICOLON_in_expression6039 |
static org.antlr.runtime.BitSet |
FOLLOW_SEMICOLON_in_expression6103 |
static org.antlr.runtime.BitSet |
FOLLOW_SEMICOLON_in_field_declaration4277 |
static org.antlr.runtime.BitSet |
FOLLOW_SEMICOLON_in_merge_point_statement5353 |
static org.antlr.runtime.BitSet |
FOLLOW_SEMICOLON_in_method_declaration4362 |
static org.antlr.runtime.BitSet |
FOLLOW_SEMICOLON_in_name_clause3897 |
static org.antlr.runtime.BitSet |
FOLLOW_separates_clause_in_simple_spec_body_clause3079 |
static org.antlr.runtime.BitSet |
FOLLOW_separates_keyword_in_loop_separates_clause5840 |
static org.antlr.runtime.BitSet |
FOLLOW_separates_keyword_in_separates_clause3162 |
static org.antlr.runtime.BitSet |
FOLLOW_set_in_expression6055 |
static org.antlr.runtime.BitSet |
FOLLOW_set_in_param_decl4609 |
static org.antlr.runtime.BitSet |
FOLLOW_SET_in_set_statement5278 |
static org.antlr.runtime.BitSet |
FOLLOW_set_statement_in_classlevel_element368 |
static org.antlr.runtime.BitSet |
FOLLOW_set_statement_in_methodlevel_element520 |
static org.antlr.runtime.BitSet |
FOLLOW_signals_clause_in_simple_spec_body_clause2892 |
static org.antlr.runtime.BitSet |
FOLLOW_signals_keyword_in_signals_clause3649 |
static org.antlr.runtime.BitSet |
FOLLOW_signals_only_clause_in_simple_spec_body_clause2910 |
static org.antlr.runtime.BitSet |
FOLLOW_signals_only_keyword_in_signals_only_clause3730 |
static org.antlr.runtime.BitSet |
FOLLOW_simple_spec_body_clause_in_simple_spec_body2789 |
static org.antlr.runtime.BitSet |
FOLLOW_simple_spec_body_in_generic_spec_body2610 |
static org.antlr.runtime.BitSet |
FOLLOW_SPEC_BIGINT_MATH_in_modifier1213 |
static org.antlr.runtime.BitSet |
FOLLOW_spec_case_in_block_loop_specification6233 |
static org.antlr.runtime.BitSet |
FOLLOW_spec_case_in_block_loop_specification6267 |
static org.antlr.runtime.BitSet |
FOLLOW_spec_case_in_method_specification1570 |
static org.antlr.runtime.BitSet |
FOLLOW_spec_case_in_method_specification1602 |
static org.antlr.runtime.BitSet |
FOLLOW_spec_header_in_generic_spec_case2186 |
static org.antlr.runtime.BitSet |
FOLLOW_SPEC_JAVA_MATH_in_modifier1175 |
static org.antlr.runtime.BitSet |
FOLLOW_SPEC_NAME_in_name_clause3891 |
static org.antlr.runtime.BitSet |
FOLLOW_SPEC_PROTECTED_in_modifier1058 |
static org.antlr.runtime.BitSet |
FOLLOW_SPEC_PUBLIC_in_modifier1077 |
static org.antlr.runtime.BitSet |
FOLLOW_SPEC_SAVE_MATH_in_modifier1194 |
static org.antlr.runtime.BitSet |
FOLLOW_spec_var_decls_in_generic_spec_case2174 |
static org.antlr.runtime.BitSet |
FOLLOW_STATIC_in_modifier1099 |
static org.antlr.runtime.BitSet |
FOLLOW_STRICTLY_PURE_in_modifier1038 |
static org.antlr.runtime.BitSet |
FOLLOW_STRING_LITERAL_in_merge_point_statement5327 |
static org.antlr.runtime.BitSet |
FOLLOW_STRING_LITERAL_in_name_clause3895 |
static org.antlr.runtime.BitSet |
FOLLOW_TWO_STATE_in_modifier1126 |
static org.antlr.runtime.BitSet |
FOLLOW_type_in_field_or_method_declaration4157 |
static org.antlr.runtime.BitSet |
FOLLOW_type_in_old_clause4079 |
static org.antlr.runtime.BitSet |
FOLLOW_UNREACHABLE_in_assert_statement6340 |
static org.antlr.runtime.BitSet |
FOLLOW_variant_function_in_loop_specification5577 |
static org.antlr.runtime.BitSet |
FOLLOW_variant_function_in_simple_spec_body_clause2954 |
static org.antlr.runtime.BitSet |
FOLLOW_when_clause_in_simple_spec_body_clause2996 |
static org.antlr.runtime.BitSet |
FOLLOW_when_keyword_in_when_clause3921 |
static org.antlr.runtime.BitSet |
FOLLOW_working_space_clause_in_simple_spec_body_clause3003 |
static org.antlr.runtime.BitSet |
FOLLOW_working_space_keyword_in_working_space_clause3970 |
static org.antlr.runtime.BitSet |
FOLLOW_writable_if_clause_in_classlevel_element342 |
static org.antlr.runtime.BitSet |
FOLLOW_WRITABLE_in_writable_if_clause5046 |
static int |
FOR_EXAMPLE |
static int |
FORALL |
static int |
GHOST |
static int |
HELPER |
static int |
HEXDIGIT |
static int |
HEXINTEGERLITERAL |
static int |
HEXNUMERAL |
static int |
IDENT |
static int |
IMPLIES_THAT |
static int |
IN |
static int |
IN_RED |
static int |
INITIALISER |
static int |
INITIALLY |
static int |
INSTANCE |
static int |
INTEGERLITERAL |
static int |
INTEGERTYPESUFFIX |
static int |
INVARIANT |
static int |
INVARIANT_RED |
static int |
JAVAOPERATOR |
static int |
JMLSPECIALSYMBOL |
static int |
LETTER |
private KeYJMLPreLexer |
lexer |
static int |
LOOP_CONTRACT |
static int |
LOOP_INVARIANT |
static int |
LOOP_INVARIANT_FREE |
static int |
LOOP_INVARIANT_RED |
static int |
LOOP_INVARIANT_REDUNDANTLY |
static int |
LOOP_VARIANT |
static int |
LOOP_VARIANT_RED |
static int |
LPAREN |
static int |
MAINTAINING |
static int |
MAINTAINING_REDUNDANTLY |
static int |
MAPS |
static int |
MAPS_RED |
static int |
MEASURED_BY |
static int |
MEASURED_BY_REDUNDANTLY |
static int |
MERGE_PARAMS |
static int |
MERGE_POINT |
static int |
MERGE_PROC |
static int |
ML_COMMENT |
static int |
MODEL |
static int |
MODEL_BEHAVIOR |
static int |
MODEL_BEHAVIOUR |
static int |
MODIFIABLE |
static int |
MODIFIABLE_RED |
static int |
MODIFIES |
static int |
MODIFIES_RED |
static int |
MONITORED |
static int |
MONITORS_FOR |
static int |
NATIVE |
static int |
NEST_END |
static int |
NEST_START |
static int |
NO_STATE |
static int |
NON_NULL |
static int |
NONZERODIGIT |
static int |
NORMAL_BEHAVIOR |
static int |
NORMAL_BEHAVIOUR |
static int |
NOWARN |
static int |
NULLABLE |
static int |
NULLABLE_BY_DEFAULT |
static int |
OCT_CHAR |
static int |
OCTALDIGIT |
static int |
OCTALINTEGERLITERAL |
static int |
OCTALNUMERAL |
static int |
OCTDIGIT |
static int |
OLD |
static int |
POST |
static int |
POST_RED |
static int |
PRE |
static int |
PRE_RED |
static int |
PRIVATE |
static int |
PROTECTED |
static int |
PUBLIC |
static int |
PURE |
static int |
READABLE |
static int |
REPRESENTS |
static int |
REPRESENTS_RED |
static int |
REQUIRES |
static int |
REQUIRES_FREE |
static int |
REQUIRES_RED |
static int |
RESPECTS |
static int |
RETURN_BEHAVIOR |
static int |
RETURN_BEHAVIOUR |
static int |
RETURNS |
static int |
RPAREN |
static int |
SEMICOLON |
static int |
SEPARATES |
static int |
SET |
static int |
SIGNALS |
static int |
SIGNALS_ONLY |
static int |
SIGNALS_ONLY_RED |
static int |
SIGNALS_RED |
static int |
SL_COMMENT |
static int |
SPEC_BIGINT_MATH |
static int |
SPEC_JAVA_MATH |
static int |
SPEC_NAME |
static int |
SPEC_PROTECTED |
static int |
SPEC_PUBLIC |
static int |
SPEC_SAFE_MATH |
static int |
SPEC_SAVE_MATH |
static int |
STATIC |
static int |
STRICTFP |
static int |
STRICTLY_PURE |
static int |
STRING_LITERAL |
static int |
SYNCHRONIZED |
static java.lang.String[] |
tokenNames |
static int |
TRANSIENT |
static int |
TWO_STATE |
static int |
UNINITIALIZED |
static int |
UNREACHABLE |
static int |
VOLATILE |
private ImmutableSet<PositionedString> |
warnings |
static int |
WHEN |
static int |
WHEN_RED |
static int |
WORKING_SPACE |
static int |
WORKING_SPACE_RED |
static int |
WRITABLE |
static int |
WS |
Modifier | Constructor and Description |
---|---|
private |
KeYJMLPreParser(KeYJMLPreLexer lexer,
java.lang.String fileName,
Position offsetPos) |
|
KeYJMLPreParser(java.lang.String comment,
java.lang.String fileName,
Position offsetPos) |
|
KeYJMLPreParser(org.antlr.runtime.TokenStream input) |
|
KeYJMLPreParser(org.antlr.runtime.TokenStream input,
org.antlr.runtime.RecognizerSharedState state) |
getCurrentInputSymbol, getMissingSymbol, getSourceName, getTokenStream, reset, setTokenStream, traceIn, traceOut
alreadyParsedRule, beginResync, combineFollows, computeContextSensitiveRuleFOLLOW, computeErrorRecoverySet, consumeUntil, consumeUntil, displayRecognitionError, emitErrorMessage, endResync, failed, getBacktrackingLevel, getErrorHeader, getErrorMessage, getNumberOfSyntaxErrors, getRuleInvocationStack, getRuleInvocationStack, getRuleMemoization, getRuleMemoizationCacheSize, getTokenErrorDisplay, match, matchAny, memoize, mismatchIsMissingToken, mismatchIsUnwantedToken, pushFollow, recover, reportError, setBacktrackingLevel, toStrings, traceIn, traceOut
public static final java.lang.String[] tokenNames
public static final int EOF
public static final int ABSTRACT
public static final int ACCESSIBLE
public static final int ACCESSIBLE_REDUNDANTLY
public static final int ALSO
public static final int ASSERT
public static final int ASSERT_REDUNDANTLY
public static final int ASSIGNABLE
public static final int ASSIGNABLE_RED
public static final int ASSIGNS
public static final int ASSIGNS_RED
public static final int ASSUME
public static final int ASSUME_REDUNDANTLY
public static final int AXIOM
public static final int AXIOM_NAME_BEGIN
public static final int AXIOM_NAME_END
public static final int BEHAVIOR
public static final int BEHAVIOUR
public static final int BODY
public static final int BRACE_DISPATCH
public static final int BREAKS
public static final int BREAK_BEHAVIOR
public static final int BREAK_BEHAVIOUR
public static final int CAPTURES
public static final int CAPTURES_RED
public static final int CHAR_LITERAL
public static final int CODE
public static final int CODE_BIGINT_MATH
public static final int CODE_JAVA_MATH
public static final int CODE_SAFE_MATH
public static final int COMMA
public static final int CONST
public static final int CONSTRAINT
public static final int CONSTRAINT_RED
public static final int CONTINUES
public static final int CONTINUE_BEHAVIOR
public static final int CONTINUE_BEHAVIOUR
public static final int DEBUG
public static final int DECIMALINTEGERLITERAL
public static final int DECREASES
public static final int DECREASES_REDUNDANTLY
public static final int DECREASING
public static final int DECREASING_REDUNDANTLY
public static final int DETERMINES
public static final int DIGIT
public static final int DIGITS
public static final int DIVERGES
public static final int DIVERGES_RED
public static final int DOT
public static final int DURATION
public static final int DURATION_RED
public static final int EMPTYBRACKETS
public static final int ENSURES
public static final int ENSURES_FREE
public static final int ENSURES_RED
public static final int EQUALITY
public static final int ESC
public static final int EXCEPTIONAL_BEHAVIOR
public static final int EXCEPTIONAL_BEHAVIOUR
public static final int EXSURES
public static final int EXSURES_RED
public static final int FINAL
public static final int FORALL
public static final int FOR_EXAMPLE
public static final int GHOST
public static final int HELPER
public static final int HEXDIGIT
public static final int HEXINTEGERLITERAL
public static final int HEXNUMERAL
public static final int IDENT
public static final int IMPLIES_THAT
public static final int IN
public static final int INITIALLY
public static final int INSTANCE
public static final int INTEGERLITERAL
public static final int INTEGERTYPESUFFIX
public static final int INVARIANT
public static final int INVARIANT_RED
public static final int IN_RED
public static final int JAVAOPERATOR
public static final int JMLSPECIALSYMBOL
public static final int LETTER
public static final int LOOP_CONTRACT
public static final int LOOP_INVARIANT
public static final int LOOP_INVARIANT_FREE
public static final int LOOP_INVARIANT_RED
public static final int LOOP_VARIANT
public static final int LOOP_VARIANT_RED
public static final int LPAREN
public static final int MAINTAINING
public static final int MAINTAINING_REDUNDANTLY
public static final int MAPS
public static final int MAPS_RED
public static final int MEASURED_BY
public static final int MEASURED_BY_REDUNDANTLY
public static final int MERGE_PARAMS
public static final int MERGE_POINT
public static final int MERGE_PROC
public static final int ML_COMMENT
public static final int MODEL
public static final int MODEL_BEHAVIOR
public static final int MODEL_BEHAVIOUR
public static final int MODIFIABLE
public static final int MODIFIABLE_RED
public static final int MODIFIES
public static final int MODIFIES_RED
public static final int MONITORED
public static final int MONITORS_FOR
public static final int NATIVE
public static final int NEST_END
public static final int NEST_START
public static final int NONZERODIGIT
public static final int NON_NULL
public static final int NORMAL_BEHAVIOR
public static final int NORMAL_BEHAVIOUR
public static final int NOWARN
public static final int NO_STATE
public static final int NULLABLE
public static final int NULLABLE_BY_DEFAULT
public static final int OCTALDIGIT
public static final int OCTALINTEGERLITERAL
public static final int OCTALNUMERAL
public static final int OCTDIGIT
public static final int OCT_CHAR
public static final int OLD
public static final int POST
public static final int POST_RED
public static final int PRE
public static final int PRE_RED
public static final int PRIVATE
public static final int PROTECTED
public static final int PUBLIC
public static final int PURE
public static final int READABLE
public static final int REPRESENTS
public static final int REPRESENTS_RED
public static final int REQUIRES
public static final int REQUIRES_FREE
public static final int REQUIRES_RED
public static final int RESPECTS
public static final int RETURNS
public static final int RETURN_BEHAVIOR
public static final int RETURN_BEHAVIOUR
public static final int RPAREN
public static final int SEMICOLON
public static final int SEPARATES
public static final int SET
public static final int SIGNALS
public static final int SIGNALS_ONLY
public static final int SIGNALS_ONLY_RED
public static final int SIGNALS_RED
public static final int SL_COMMENT
public static final int SPEC_BIGINT_MATH
public static final int SPEC_JAVA_MATH
public static final int SPEC_NAME
public static final int SPEC_PROTECTED
public static final int SPEC_PUBLIC
public static final int SPEC_SAFE_MATH
public static final int STATIC
public static final int STRICTFP
public static final int STRICTLY_PURE
public static final int STRING_LITERAL
public static final int SYNCHRONIZED
public static final int TRANSIENT
public static final int TWO_STATE
public static final int UNINITIALIZED
public static final int UNREACHABLE
public static final int VOLATILE
public static final int WHEN
public static final int WHEN_RED
public static final int WORKING_SPACE
public static final int WORKING_SPACE_RED
public static final int WRITABLE
public static final int WS
public static final int AXION_NAME_END
public static final int CODE_SAVE_MATH
public static final int INITIALISER
public static final int LOOP_INVARIANT_REDUNDANTLY
public static final int SPEC_SAVE_MATH
private KeYJMLPreLexer lexer
private SLTranslationExceptionManager excManager
private ImmutableSet<PositionedString> warnings
protected KeYJMLPreParser.DFA1 dfa1
protected KeYJMLPreParser.DFA2 dfa2
protected KeYJMLPreParser.DFA3 dfa3
protected KeYJMLPreParser.DFA5 dfa5
protected KeYJMLPreParser.DFA9 dfa9
protected KeYJMLPreParser.DFA15 dfa15
protected KeYJMLPreParser.DFA18 dfa18
protected KeYJMLPreParser.DFA23 dfa23
protected KeYJMLPreParser.DFA39 dfa39
protected KeYJMLPreParser.DFA43 dfa43
static final java.lang.String DFA1_eotS
static final java.lang.String DFA1_eofS
static final java.lang.String DFA1_minS
static final java.lang.String DFA1_maxS
static final java.lang.String DFA1_acceptS
static final java.lang.String DFA1_specialS
static final java.lang.String[] DFA1_transitionS
static final short[] DFA1_eot
static final short[] DFA1_eof
static final char[] DFA1_min
static final char[] DFA1_max
static final short[] DFA1_accept
static final short[] DFA1_special
static final short[][] DFA1_transition
static final java.lang.String DFA2_eotS
static final java.lang.String DFA2_eofS
static final java.lang.String DFA2_minS
static final java.lang.String DFA2_maxS
static final java.lang.String DFA2_acceptS
static final java.lang.String DFA2_specialS
static final java.lang.String[] DFA2_transitionS
static final short[] DFA2_eot
static final short[] DFA2_eof
static final char[] DFA2_min
static final char[] DFA2_max
static final short[] DFA2_accept
static final short[] DFA2_special
static final short[][] DFA2_transition
static final java.lang.String DFA3_eotS
static final java.lang.String DFA3_eofS
static final java.lang.String DFA3_minS
static final java.lang.String DFA3_maxS
static final java.lang.String DFA3_acceptS
static final java.lang.String DFA3_specialS
static final java.lang.String[] DFA3_transitionS
static final short[] DFA3_eot
static final short[] DFA3_eof
static final char[] DFA3_min
static final char[] DFA3_max
static final short[] DFA3_accept
static final short[] DFA3_special
static final short[][] DFA3_transition
static final java.lang.String DFA5_eotS
static final java.lang.String DFA5_eofS
static final java.lang.String DFA5_minS
static final java.lang.String DFA5_maxS
static final java.lang.String DFA5_acceptS
static final java.lang.String DFA5_specialS
static final java.lang.String[] DFA5_transitionS
static final short[] DFA5_eot
static final short[] DFA5_eof
static final char[] DFA5_min
static final char[] DFA5_max
static final short[] DFA5_accept
static final short[] DFA5_special
static final short[][] DFA5_transition
static final java.lang.String DFA9_eotS
static final java.lang.String DFA9_eofS
static final java.lang.String DFA9_minS
static final java.lang.String DFA9_maxS
static final java.lang.String DFA9_acceptS
static final java.lang.String DFA9_specialS
static final java.lang.String[] DFA9_transitionS
static final short[] DFA9_eot
static final short[] DFA9_eof
static final char[] DFA9_min
static final char[] DFA9_max
static final short[] DFA9_accept
static final short[] DFA9_special
static final short[][] DFA9_transition
static final java.lang.String DFA15_eotS
static final java.lang.String DFA15_eofS
static final java.lang.String DFA15_minS
static final java.lang.String DFA15_maxS
static final java.lang.String DFA15_acceptS
static final java.lang.String DFA15_specialS
static final java.lang.String[] DFA15_transitionS
static final short[] DFA15_eot
static final short[] DFA15_eof
static final char[] DFA15_min
static final char[] DFA15_max
static final short[] DFA15_accept
static final short[] DFA15_special
static final short[][] DFA15_transition
static final java.lang.String DFA18_eotS
static final java.lang.String DFA18_eofS
static final java.lang.String DFA18_minS
static final java.lang.String DFA18_maxS
static final java.lang.String DFA18_acceptS
static final java.lang.String DFA18_specialS
static final java.lang.String[] DFA18_transitionS
static final short[] DFA18_eot
static final short[] DFA18_eof
static final char[] DFA18_min
static final char[] DFA18_max
static final short[] DFA18_accept
static final short[] DFA18_special
static final short[][] DFA18_transition
static final java.lang.String DFA23_eotS
static final java.lang.String DFA23_eofS
static final java.lang.String DFA23_minS
static final java.lang.String DFA23_maxS
static final java.lang.String DFA23_acceptS
static final java.lang.String DFA23_specialS
static final java.lang.String[] DFA23_transitionS
static final short[] DFA23_eot
static final short[] DFA23_eof
static final char[] DFA23_min
static final char[] DFA23_max
static final short[] DFA23_accept
static final short[] DFA23_special
static final short[][] DFA23_transition
static final java.lang.String DFA39_eotS
static final java.lang.String DFA39_eofS
static final java.lang.String DFA39_minS
static final java.lang.String DFA39_maxS
static final java.lang.String DFA39_acceptS
static final java.lang.String DFA39_specialS
static final java.lang.String[] DFA39_transitionS
static final short[] DFA39_eot
static final short[] DFA39_eof
static final char[] DFA39_min
static final char[] DFA39_max
static final short[] DFA39_accept
static final short[] DFA39_special
static final short[][] DFA39_transition
static final java.lang.String DFA43_eotS
static final java.lang.String DFA43_eofS
static final java.lang.String DFA43_minS
static final java.lang.String DFA43_maxS
static final java.lang.String DFA43_acceptS
static final java.lang.String DFA43_specialS
static final java.lang.String[] DFA43_transitionS
static final short[] DFA43_eot
static final short[] DFA43_eof
static final char[] DFA43_min
static final char[] DFA43_max
static final short[] DFA43_accept
static final short[] DFA43_special
static final short[][] DFA43_transition
public static final org.antlr.runtime.BitSet FOLLOW_modifiers_in_classlevel_comment115
public static final org.antlr.runtime.BitSet FOLLOW_classlevel_element_in_classlevel_comment131
public static final org.antlr.runtime.BitSet FOLLOW_modifiers_in_classlevel_comment150
public static final org.antlr.runtime.BitSet FOLLOW_EOF_in_classlevel_comment163
public static final org.antlr.runtime.BitSet FOLLOW_class_invariant_in_classlevel_element204
public static final org.antlr.runtime.BitSet FOLLOW_depends_clause_in_classlevel_element225
public static final org.antlr.runtime.BitSet FOLLOW_method_specification_in_classlevel_element238
public static final org.antlr.runtime.BitSet FOLLOW_field_or_method_declaration_in_classlevel_element251
public static final org.antlr.runtime.BitSet FOLLOW_represents_clause_in_classlevel_element264
public static final org.antlr.runtime.BitSet FOLLOW_history_constraint_in_classlevel_element277
public static final org.antlr.runtime.BitSet FOLLOW_initially_clause_in_classlevel_element290
public static final org.antlr.runtime.BitSet FOLLOW_class_axiom_in_classlevel_element303
public static final org.antlr.runtime.BitSet FOLLOW_monitors_for_clause_in_classlevel_element316
public static final org.antlr.runtime.BitSet FOLLOW_readable_if_clause_in_classlevel_element329
public static final org.antlr.runtime.BitSet FOLLOW_writable_if_clause_in_classlevel_element342
public static final org.antlr.runtime.BitSet FOLLOW_datagroup_clause_in_classlevel_element355
public static final org.antlr.runtime.BitSet FOLLOW_set_statement_in_classlevel_element368
public static final org.antlr.runtime.BitSet FOLLOW_assert_statement_in_classlevel_element385
public static final org.antlr.runtime.BitSet FOLLOW_assume_statement_in_classlevel_element399
public static final org.antlr.runtime.BitSet FOLLOW_nowarn_pragma_in_classlevel_element413
public static final org.antlr.runtime.BitSet FOLLOW_modifiers_in_methodlevel_comment448
public static final org.antlr.runtime.BitSet FOLLOW_methodlevel_element_in_methodlevel_comment453
public static final org.antlr.runtime.BitSet FOLLOW_EOF_in_methodlevel_comment466
public static final org.antlr.runtime.BitSet FOLLOW_field_or_method_declaration_in_methodlevel_element507
public static final org.antlr.runtime.BitSet FOLLOW_set_statement_in_methodlevel_element520
public static final org.antlr.runtime.BitSet FOLLOW_merge_point_statement_in_methodlevel_element533
public static final org.antlr.runtime.BitSet FOLLOW_loop_specification_in_methodlevel_element546
public static final org.antlr.runtime.BitSet FOLLOW_assert_statement_in_methodlevel_element559
public static final org.antlr.runtime.BitSet FOLLOW_assume_statement_in_methodlevel_element572
public static final org.antlr.runtime.BitSet FOLLOW_nowarn_pragma_in_methodlevel_element585
public static final org.antlr.runtime.BitSet FOLLOW_debug_statement_in_methodlevel_element598
public static final org.antlr.runtime.BitSet FOLLOW_block_specification_in_methodlevel_element611
public static final org.antlr.runtime.BitSet FOLLOW_block_loop_specification_in_methodlevel_element624
public static final org.antlr.runtime.BitSet FOLLOW_modifier_in_modifiers674
public static final org.antlr.runtime.BitSet FOLLOW_ABSTRACT_in_modifier707
public static final org.antlr.runtime.BitSet FOLLOW_FINAL_in_modifier732
public static final org.antlr.runtime.BitSet FOLLOW_GHOST_in_modifier760
public static final org.antlr.runtime.BitSet FOLLOW_HELPER_in_modifier788
public static final org.antlr.runtime.BitSet FOLLOW_INSTANCE_in_modifier815
public static final org.antlr.runtime.BitSet FOLLOW_MODEL_in_modifier840
public static final org.antlr.runtime.BitSet FOLLOW_NON_NULL_in_modifier868
public static final org.antlr.runtime.BitSet FOLLOW_NULLABLE_in_modifier893
public static final org.antlr.runtime.BitSet FOLLOW_NULLABLE_BY_DEFAULT_in_modifier918
public static final org.antlr.runtime.BitSet FOLLOW_PRIVATE_in_modifier932
public static final org.antlr.runtime.BitSet FOLLOW_PROTECTED_in_modifier958
public static final org.antlr.runtime.BitSet FOLLOW_PUBLIC_in_modifier982
public static final org.antlr.runtime.BitSet FOLLOW_PURE_in_modifier1009
public static final org.antlr.runtime.BitSet FOLLOW_STRICTLY_PURE_in_modifier1038
public static final org.antlr.runtime.BitSet FOLLOW_SPEC_PROTECTED_in_modifier1058
public static final org.antlr.runtime.BitSet FOLLOW_SPEC_PUBLIC_in_modifier1077
public static final org.antlr.runtime.BitSet FOLLOW_STATIC_in_modifier1099
public static final org.antlr.runtime.BitSet FOLLOW_TWO_STATE_in_modifier1126
public static final org.antlr.runtime.BitSet FOLLOW_NO_STATE_in_modifier1150
public static final org.antlr.runtime.BitSet FOLLOW_SPEC_JAVA_MATH_in_modifier1175
public static final org.antlr.runtime.BitSet FOLLOW_SPEC_SAVE_MATH_in_modifier1194
public static final org.antlr.runtime.BitSet FOLLOW_SPEC_BIGINT_MATH_in_modifier1213
public static final org.antlr.runtime.BitSet FOLLOW_CODE_JAVA_MATH_in_modifier1230
public static final org.antlr.runtime.BitSet FOLLOW_CODE_SAVE_MATH_in_modifier1249
public static final org.antlr.runtime.BitSet FOLLOW_CODE_BIGINT_MATH_in_modifier1268
public static final org.antlr.runtime.BitSet FOLLOW_invariant_keyword_in_class_invariant1308
public static final org.antlr.runtime.BitSet FOLLOW_expression_in_class_invariant1317
public static final org.antlr.runtime.BitSet FOLLOW_AXIOM_NAME_BEGIN_in_axiom_name1346
public static final org.antlr.runtime.BitSet FOLLOW_IDENT_in_axiom_name1350
public static final org.antlr.runtime.BitSet FOLLOW_AXIOM_NAME_END_in_axiom_name1352
public static final org.antlr.runtime.BitSet FOLLOW_AXIOM_in_class_axiom1442
public static final org.antlr.runtime.BitSet FOLLOW_expression_in_class_axiom1446
public static final org.antlr.runtime.BitSet FOLLOW_INITIALLY_in_initially_clause1511
public static final org.antlr.runtime.BitSet FOLLOW_expression_in_initially_clause1515
public static final org.antlr.runtime.BitSet FOLLOW_also_keyword_in_method_specification1560
public static final org.antlr.runtime.BitSet FOLLOW_spec_case_in_method_specification1570
public static final org.antlr.runtime.BitSet FOLLOW_also_keyword_in_method_specification1596
public static final org.antlr.runtime.BitSet FOLLOW_spec_case_in_method_specification1602
public static final org.antlr.runtime.BitSet FOLLOW_lightweight_spec_case_in_spec_case1676
public static final org.antlr.runtime.BitSet FOLLOW_heavyweight_spec_case_in_spec_case1688
public static final org.antlr.runtime.BitSet FOLLOW_generic_spec_case_in_lightweight_spec_case1731
public static final org.antlr.runtime.BitSet FOLLOW_modifier_in_heavyweight_spec_case1775
public static final org.antlr.runtime.BitSet FOLLOW_behavior_spec_case_in_heavyweight_spec_case1795
public static final org.antlr.runtime.BitSet FOLLOW_break_behavior_spec_case_in_heavyweight_spec_case1809
public static final org.antlr.runtime.BitSet FOLLOW_continue_behavior_spec_case_in_heavyweight_spec_case1823
public static final org.antlr.runtime.BitSet FOLLOW_exceptional_behavior_spec_case_in_heavyweight_spec_case1837
public static final org.antlr.runtime.BitSet FOLLOW_normal_behavior_spec_case_in_heavyweight_spec_case1847
public static final org.antlr.runtime.BitSet FOLLOW_model_behavior_spec_case_in_heavyweight_spec_case1857
public static final org.antlr.runtime.BitSet FOLLOW_return_behavior_spec_case_in_heavyweight_spec_case1867
public static final org.antlr.runtime.BitSet FOLLOW_behavior_keyword_in_behavior_spec_case1909
public static final org.antlr.runtime.BitSet FOLLOW_generic_spec_case_in_behavior_spec_case1917
public static final org.antlr.runtime.BitSet FOLLOW_normal_behavior_keyword_in_normal_behavior_spec_case1973
public static final org.antlr.runtime.BitSet FOLLOW_generic_spec_case_in_normal_behavior_spec_case1981
public static final org.antlr.runtime.BitSet FOLLOW_model_behavior_keyword_in_model_behavior_spec_case2036
public static final org.antlr.runtime.BitSet FOLLOW_generic_spec_case_in_model_behavior_spec_case2044
public static final org.antlr.runtime.BitSet FOLLOW_exceptional_behavior_keyword_in_exceptional_behavior_spec_case2103
public static final org.antlr.runtime.BitSet FOLLOW_generic_spec_case_in_exceptional_behavior_spec_case2111
public static final org.antlr.runtime.BitSet FOLLOW_spec_var_decls_in_generic_spec_case2174
public static final org.antlr.runtime.BitSet FOLLOW_spec_header_in_generic_spec_case2186
public static final org.antlr.runtime.BitSet FOLLOW_free_spec_header_in_generic_spec_case2197
public static final org.antlr.runtime.BitSet FOLLOW_generic_spec_body_in_generic_spec_case2230
public static final org.antlr.runtime.BitSet FOLLOW_generic_spec_body_in_generic_spec_case2256
public static final org.antlr.runtime.BitSet FOLLOW_old_clause_in_spec_var_decls2302
public static final org.antlr.runtime.BitSet FOLLOW_FORALL_in_spec_var_decls2337
public static final org.antlr.runtime.BitSet FOLLOW_expression_in_spec_var_decls2341
public static final org.antlr.runtime.BitSet FOLLOW_requires_clause_in_spec_header2398
public static final org.antlr.runtime.BitSet FOLLOW_requires_free_clause_in_free_spec_header2452
public static final org.antlr.runtime.BitSet FOLLOW_requires_keyword_in_requires_clause2496
public static final org.antlr.runtime.BitSet FOLLOW_expression_in_requires_clause2500
public static final org.antlr.runtime.BitSet FOLLOW_REQUIRES_FREE_in_requires_free_clause2567
public static final org.antlr.runtime.BitSet FOLLOW_expression_in_requires_free_clause2571
public static final org.antlr.runtime.BitSet FOLLOW_simple_spec_body_in_generic_spec_body2610
public static final org.antlr.runtime.BitSet FOLLOW_NEST_START_in_generic_spec_body2631
public static final org.antlr.runtime.BitSet FOLLOW_generic_spec_case_seq_in_generic_spec_body2640
public static final org.antlr.runtime.BitSet FOLLOW_NEST_END_in_generic_spec_body2648
public static final org.antlr.runtime.BitSet FOLLOW_generic_spec_case_in_generic_spec_case_seq2691
public static final org.antlr.runtime.BitSet FOLLOW_also_keyword_in_generic_spec_case_seq2709
public static final org.antlr.runtime.BitSet FOLLOW_generic_spec_case_in_generic_spec_case_seq2723
public static final org.antlr.runtime.BitSet FOLLOW_simple_spec_body_clause_in_simple_spec_body2789
public static final org.antlr.runtime.BitSet FOLLOW_assignable_clause_in_simple_spec_body_clause2831
public static final org.antlr.runtime.BitSet FOLLOW_accessible_clause_in_simple_spec_body_clause2846
public static final org.antlr.runtime.BitSet FOLLOW_ensures_clause_in_simple_spec_body_clause2861
public static final org.antlr.runtime.BitSet FOLLOW_ensures_free_clause_in_simple_spec_body_clause2879
public static final org.antlr.runtime.BitSet FOLLOW_signals_clause_in_simple_spec_body_clause2892
public static final org.antlr.runtime.BitSet FOLLOW_signals_only_clause_in_simple_spec_body_clause2910
public static final org.antlr.runtime.BitSet FOLLOW_diverges_clause_in_simple_spec_body_clause2923
public static final org.antlr.runtime.BitSet FOLLOW_measured_by_clause_in_simple_spec_body_clause2940
public static final org.antlr.runtime.BitSet FOLLOW_variant_function_in_simple_spec_body_clause2954
public static final org.antlr.runtime.BitSet FOLLOW_name_clause_in_simple_spec_body_clause2970
public static final org.antlr.runtime.BitSet FOLLOW_captures_clause_in_simple_spec_body_clause2989
public static final org.antlr.runtime.BitSet FOLLOW_when_clause_in_simple_spec_body_clause2996
public static final org.antlr.runtime.BitSet FOLLOW_working_space_clause_in_simple_spec_body_clause3003
public static final org.antlr.runtime.BitSet FOLLOW_duration_clause_in_simple_spec_body_clause3010
public static final org.antlr.runtime.BitSet FOLLOW_breaks_clause_in_simple_spec_body_clause3019
public static final org.antlr.runtime.BitSet FOLLOW_continues_clause_in_simple_spec_body_clause3038
public static final org.antlr.runtime.BitSet FOLLOW_returns_clause_in_simple_spec_body_clause3054
public static final org.antlr.runtime.BitSet FOLLOW_separates_clause_in_simple_spec_body_clause3079
public static final org.antlr.runtime.BitSet FOLLOW_determines_clause_in_simple_spec_body_clause3102
public static final org.antlr.runtime.BitSet FOLLOW_separates_keyword_in_separates_clause3162
public static final org.antlr.runtime.BitSet FOLLOW_expression_in_separates_clause3166
public static final org.antlr.runtime.BitSet FOLLOW_determines_keyword_in_determines_clause3230
public static final org.antlr.runtime.BitSet FOLLOW_expression_in_determines_clause3234
public static final org.antlr.runtime.BitSet FOLLOW_DETERMINES_in_determines_keyword3254
public static final org.antlr.runtime.BitSet FOLLOW_assignable_keyword_in_assignable_clause3288
public static final org.antlr.runtime.BitSet FOLLOW_expression_in_assignable_clause3292
public static final org.antlr.runtime.BitSet FOLLOW_accessible_keyword_in_accessible_clause3409
public static final org.antlr.runtime.BitSet FOLLOW_expression_in_accessible_clause3413
public static final org.antlr.runtime.BitSet FOLLOW_measured_by_keyword_in_measured_by_clause3478
public static final org.antlr.runtime.BitSet FOLLOW_expression_in_measured_by_clause3482
public static final org.antlr.runtime.BitSet FOLLOW_ensures_keyword_in_ensures_clause3546
public static final org.antlr.runtime.BitSet FOLLOW_expression_in_ensures_clause3550
public static final org.antlr.runtime.BitSet FOLLOW_ENSURES_FREE_in_ensures_free_clause3609
public static final org.antlr.runtime.BitSet FOLLOW_expression_in_ensures_free_clause3613
public static final org.antlr.runtime.BitSet FOLLOW_signals_keyword_in_signals_clause3649
public static final org.antlr.runtime.BitSet FOLLOW_expression_in_signals_clause3653
public static final org.antlr.runtime.BitSet FOLLOW_signals_only_keyword_in_signals_only_clause3730
public static final org.antlr.runtime.BitSet FOLLOW_expression_in_signals_only_clause3734
public static final org.antlr.runtime.BitSet FOLLOW_diverges_keyword_in_diverges_clause3791
public static final org.antlr.runtime.BitSet FOLLOW_expression_in_diverges_clause3795
public static final org.antlr.runtime.BitSet FOLLOW_captures_keyword_in_captures_clause3834
public static final org.antlr.runtime.BitSet FOLLOW_expression_in_captures_clause3838
public static final org.antlr.runtime.BitSet FOLLOW_SPEC_NAME_in_name_clause3891
public static final org.antlr.runtime.BitSet FOLLOW_STRING_LITERAL_in_name_clause3895
public static final org.antlr.runtime.BitSet FOLLOW_SEMICOLON_in_name_clause3897
public static final org.antlr.runtime.BitSet FOLLOW_when_keyword_in_when_clause3921
public static final org.antlr.runtime.BitSet FOLLOW_expression_in_when_clause3925
public static final org.antlr.runtime.BitSet FOLLOW_working_space_keyword_in_working_space_clause3970
public static final org.antlr.runtime.BitSet FOLLOW_expression_in_working_space_clause3974
public static final org.antlr.runtime.BitSet FOLLOW_duration_keyword_in_duration_clause4019
public static final org.antlr.runtime.BitSet FOLLOW_expression_in_duration_clause4023
public static final org.antlr.runtime.BitSet FOLLOW_OLD_in_old_clause4070
public static final org.antlr.runtime.BitSet FOLLOW_modifiers_in_old_clause4074
public static final org.antlr.runtime.BitSet FOLLOW_type_in_old_clause4079
public static final org.antlr.runtime.BitSet FOLLOW_IDENT_in_old_clause4084
public static final org.antlr.runtime.BitSet FOLLOW_INITIALISER_in_old_clause4089
public static final org.antlr.runtime.BitSet FOLLOW_IDENT_in_type4121
public static final org.antlr.runtime.BitSet FOLLOW_EMPTYBRACKETS_in_type4132
public static final org.antlr.runtime.BitSet FOLLOW_type_in_field_or_method_declaration4157
public static final org.antlr.runtime.BitSet FOLLOW_IDENT_in_field_or_method_declaration4162
public static final org.antlr.runtime.BitSet FOLLOW_method_declaration_in_field_or_method_declaration4181
public static final org.antlr.runtime.BitSet FOLLOW_field_declaration_in_field_or_method_declaration4204
public static final org.antlr.runtime.BitSet FOLLOW_EMPTYBRACKETS_in_field_declaration4246
public static final org.antlr.runtime.BitSet FOLLOW_initialiser_in_field_declaration4265
public static final org.antlr.runtime.BitSet FOLLOW_SEMICOLON_in_field_declaration4277
public static final org.antlr.runtime.BitSet FOLLOW_param_list_in_method_declaration4326
public static final org.antlr.runtime.BitSet FOLLOW_BODY_in_method_declaration4345
public static final org.antlr.runtime.BitSet FOLLOW_SEMICOLON_in_method_declaration4362
public static final org.antlr.runtime.BitSet FOLLOW_LPAREN_in_param_list4411
public static final org.antlr.runtime.BitSet FOLLOW_param_decl_in_param_list4439
public static final org.antlr.runtime.BitSet FOLLOW_COMMA_in_param_list4475
public static final org.antlr.runtime.BitSet FOLLOW_param_decl_in_param_list4495
public static final org.antlr.runtime.BitSet FOLLOW_RPAREN_in_param_list4551
public static final org.antlr.runtime.BitSet FOLLOW_set_in_param_decl4609
public static final org.antlr.runtime.BitSet FOLLOW_IDENT_in_param_decl4653
public static final org.antlr.runtime.BitSet FOLLOW_AXIOM_NAME_BEGIN_in_param_decl4687
public static final org.antlr.runtime.BitSet FOLLOW_AXION_NAME_END_in_param_decl4702
public static final org.antlr.runtime.BitSet FOLLOW_EMPTYBRACKETS_in_param_decl4717
public static final org.antlr.runtime.BitSet FOLLOW_IDENT_in_param_decl4760
public static final org.antlr.runtime.BitSet FOLLOW_represents_keyword_in_represents_clause4804
public static final org.antlr.runtime.BitSet FOLLOW_expression_in_represents_clause4808
public static final org.antlr.runtime.BitSet FOLLOW_accessible_keyword_in_depends_clause4872
public static final org.antlr.runtime.BitSet FOLLOW_expression_in_depends_clause4876
public static final org.antlr.runtime.BitSet FOLLOW_constraint_keyword_in_history_constraint4912
public static final org.antlr.runtime.BitSet FOLLOW_expression_in_history_constraint4916
public static final org.antlr.runtime.BitSet FOLLOW_MONITORS_FOR_in_monitors_for_clause4976
public static final org.antlr.runtime.BitSet FOLLOW_expression_in_monitors_for_clause4980
public static final org.antlr.runtime.BitSet FOLLOW_READABLE_in_readable_if_clause5011
public static final org.antlr.runtime.BitSet FOLLOW_expression_in_readable_if_clause5015
public static final org.antlr.runtime.BitSet FOLLOW_WRITABLE_in_writable_if_clause5046
public static final org.antlr.runtime.BitSet FOLLOW_expression_in_writable_if_clause5050
public static final org.antlr.runtime.BitSet FOLLOW_in_group_clause_in_datagroup_clause5081
public static final org.antlr.runtime.BitSet FOLLOW_maps_into_clause_in_datagroup_clause5085
public static final org.antlr.runtime.BitSet FOLLOW_in_keyword_in_in_group_clause5104
public static final org.antlr.runtime.BitSet FOLLOW_expression_in_in_group_clause5108
public static final org.antlr.runtime.BitSet FOLLOW_maps_keyword_in_maps_into_clause5152
public static final org.antlr.runtime.BitSet FOLLOW_expression_in_maps_into_clause5156
public static final org.antlr.runtime.BitSet FOLLOW_NOWARN_in_nowarn_pragma5207
public static final org.antlr.runtime.BitSet FOLLOW_expression_in_nowarn_pragma5211
public static final org.antlr.runtime.BitSet FOLLOW_DEBUG_in_debug_statement5244
public static final org.antlr.runtime.BitSet FOLLOW_expression_in_debug_statement5248
public static final org.antlr.runtime.BitSet FOLLOW_SET_in_set_statement5278
public static final org.antlr.runtime.BitSet FOLLOW_expression_in_set_statement5282
public static final org.antlr.runtime.BitSet FOLLOW_MERGE_POINT_in_merge_point_statement5311
public static final org.antlr.runtime.BitSet FOLLOW_MERGE_PROC_in_merge_point_statement5318
public static final org.antlr.runtime.BitSet FOLLOW_STRING_LITERAL_in_merge_point_statement5327
public static final org.antlr.runtime.BitSet FOLLOW_MERGE_PARAMS_in_merge_point_statement5337
public static final org.antlr.runtime.BitSet FOLLOW_BODY_in_merge_point_statement5344
public static final org.antlr.runtime.BitSet FOLLOW_SEMICOLON_in_merge_point_statement5353
public static final org.antlr.runtime.BitSet FOLLOW_loop_invariant_in_loop_specification5397
public static final org.antlr.runtime.BitSet FOLLOW_loop_invariant_free_in_loop_specification5416
public static final org.antlr.runtime.BitSet FOLLOW_loop_invariant_in_loop_specification5462
public static final org.antlr.runtime.BitSet FOLLOW_loop_invariant_free_in_loop_specification5486
public static final org.antlr.runtime.BitSet FOLLOW_loop_separates_clause_in_loop_specification5510
public static final org.antlr.runtime.BitSet FOLLOW_loop_determines_clause_in_loop_specification5533
public static final org.antlr.runtime.BitSet FOLLOW_assignable_clause_in_loop_specification5556
public static final org.antlr.runtime.BitSet FOLLOW_variant_function_in_loop_specification5577
public static final org.antlr.runtime.BitSet FOLLOW_maintaining_keyword_in_loop_invariant5618
public static final org.antlr.runtime.BitSet FOLLOW_expression_in_loop_invariant5622
public static final org.antlr.runtime.BitSet FOLLOW_LOOP_INVARIANT_FREE_in_loop_invariant_free5650
public static final org.antlr.runtime.BitSet FOLLOW_expression_in_loop_invariant_free5654
public static final org.antlr.runtime.BitSet FOLLOW_decreasing_keyword_in_variant_function5731
public static final org.antlr.runtime.BitSet FOLLOW_expression_in_variant_function5735
public static final org.antlr.runtime.BitSet FOLLOW_separates_keyword_in_loop_separates_clause5840
public static final org.antlr.runtime.BitSet FOLLOW_expression_in_loop_separates_clause5844
public static final org.antlr.runtime.BitSet FOLLOW_determines_keyword_in_loop_determines_clause5880
public static final org.antlr.runtime.BitSet FOLLOW_expression_in_loop_determines_clause5884
public static final org.antlr.runtime.BitSet FOLLOW_assume_keyword_in_assume_statement5917
public static final org.antlr.runtime.BitSet FOLLOW_expression_in_assume_statement5921
public static final org.antlr.runtime.BitSet FOLLOW_LPAREN_in_expression6001
public static final org.antlr.runtime.BitSet FOLLOW_RPAREN_in_expression6019
public static final org.antlr.runtime.BitSet FOLLOW_SEMICOLON_in_expression6039
public static final org.antlr.runtime.BitSet FOLLOW_set_in_expression6055
public static final org.antlr.runtime.BitSet FOLLOW_SEMICOLON_in_expression6103
public static final org.antlr.runtime.BitSet FOLLOW_EQUALITY_in_initialiser6136
public static final org.antlr.runtime.BitSet FOLLOW_expression_in_initialiser6140
public static final org.antlr.runtime.BitSet FOLLOW_method_specification_in_block_specification6188
public static final org.antlr.runtime.BitSet FOLLOW_loop_contract_keyword_in_block_loop_specification6229
public static final org.antlr.runtime.BitSet FOLLOW_spec_case_in_block_loop_specification6233
public static final org.antlr.runtime.BitSet FOLLOW_also_keyword_in_block_loop_specification6259
public static final org.antlr.runtime.BitSet FOLLOW_loop_contract_keyword_in_block_loop_specification6263
public static final org.antlr.runtime.BitSet FOLLOW_spec_case_in_block_loop_specification6267
public static final org.antlr.runtime.BitSet FOLLOW_LOOP_CONTRACT_in_loop_contract_keyword6294
public static final org.antlr.runtime.BitSet FOLLOW_assert_keyword_in_assert_statement6318
public static final org.antlr.runtime.BitSet FOLLOW_expression_in_assert_statement6322
public static final org.antlr.runtime.BitSet FOLLOW_UNREACHABLE_in_assert_statement6340
public static final org.antlr.runtime.BitSet FOLLOW_SEMICOLON_in_assert_statement6342
public static final org.antlr.runtime.BitSet FOLLOW_breaks_keyword_in_breaks_clause6397
public static final org.antlr.runtime.BitSet FOLLOW_expression_in_breaks_clause6401
public static final org.antlr.runtime.BitSet FOLLOW_BREAKS_in_breaks_keyword6414
public static final org.antlr.runtime.BitSet FOLLOW_continues_keyword_in_continues_clause6445
public static final org.antlr.runtime.BitSet FOLLOW_expression_in_continues_clause6449
public static final org.antlr.runtime.BitSet FOLLOW_CONTINUES_in_continues_keyword6462
public static final org.antlr.runtime.BitSet FOLLOW_returns_keyword_in_returns_clause6493
public static final org.antlr.runtime.BitSet FOLLOW_expression_in_returns_clause6497
public static final org.antlr.runtime.BitSet FOLLOW_RETURNS_in_returns_keyword6510
public static final org.antlr.runtime.BitSet FOLLOW_break_behavior_keyword_in_break_behavior_spec_case6545
public static final org.antlr.runtime.BitSet FOLLOW_generic_spec_case_in_break_behavior_spec_case6553
public static final org.antlr.runtime.BitSet FOLLOW_continue_behavior_keyword_in_continue_behavior_spec_case6608
public static final org.antlr.runtime.BitSet FOLLOW_generic_spec_case_in_continue_behavior_spec_case6616
public static final org.antlr.runtime.BitSet FOLLOW_return_behavior_keyword_in_return_behavior_spec_case6671
public static final org.antlr.runtime.BitSet FOLLOW_generic_spec_case_in_return_behavior_spec_case6679
public static final org.antlr.runtime.BitSet FOLLOW_accessible_keyword_in_synpred1_KeYJMLPreParser216
public static final org.antlr.runtime.BitSet FOLLOW_expression_in_synpred1_KeYJMLPreParser218
public static final org.antlr.runtime.BitSet FOLLOW_LPAREN_in_synpred2_KeYJMLPreParser4172
public KeYJMLPreParser(org.antlr.runtime.TokenStream input)
public KeYJMLPreParser(org.antlr.runtime.TokenStream input, org.antlr.runtime.RecognizerSharedState state)
private KeYJMLPreParser(KeYJMLPreLexer lexer, java.lang.String fileName, Position offsetPos)
public KeYJMLPreParser(java.lang.String comment, java.lang.String fileName, Position offsetPos)
public org.antlr.runtime.Parser[] getDelegates()
public java.lang.String[] getTokenNames()
getTokenNames
in class org.antlr.runtime.BaseRecognizer
public java.lang.String getGrammarFileName()
getGrammarFileName
in class org.antlr.runtime.BaseRecognizer
private PositionedString createPositionedString(java.lang.String text, org.antlr.runtime.Token t)
private PositionedString createPositionedString(java.lang.String text, Position pos)
private void raiseError(java.lang.String msg) throws SLTranslationException
SLTranslationException
private void raiseNotSupported(java.lang.String feature) throws SLTranslationException
SLTranslationException
public ImmutableList<TextualJMLConstruct> parseClasslevelComment() throws SLTranslationException
SLTranslationException
public ImmutableList<TextualJMLConstruct> parseMethodlevelComment() throws SLTranslationException
SLTranslationException
public ImmutableSet<PositionedString> getWarnings()
private PositionedString flipHeaps(java.lang.String declString, PositionedString result)
private PositionedString flipHeaps(java.lang.String declString, PositionedString result, boolean allowPreHeaps)
protected java.lang.Object recoverFromMismatchedToken(org.antlr.runtime.IntStream input, int ttype, org.antlr.runtime.BitSet follow) throws org.antlr.runtime.RecognitionException
recoverFromMismatchedToken
in class org.antlr.runtime.BaseRecognizer
org.antlr.runtime.RecognitionException
public java.lang.Object recoverFromMismatchedSet(org.antlr.runtime.IntStream input, org.antlr.runtime.RecognitionException e, org.antlr.runtime.BitSet follow) throws org.antlr.runtime.RecognitionException
recoverFromMismatchedSet
in class org.antlr.runtime.BaseRecognizer
org.antlr.runtime.RecognitionException
public final ImmutableList<TextualJMLConstruct> classlevel_comment() throws SLTranslationException, org.antlr.runtime.RecognitionException
SLTranslationException
org.antlr.runtime.RecognitionException
public final ImmutableList<TextualJMLConstruct> classlevel_element(ImmutableList<java.lang.String> mods) throws SLTranslationException, org.antlr.runtime.RecognitionException
SLTranslationException
org.antlr.runtime.RecognitionException
public final ImmutableList<TextualJMLConstruct> methodlevel_comment() throws SLTranslationException, org.antlr.runtime.RecognitionException
SLTranslationException
org.antlr.runtime.RecognitionException
public final ImmutableList<TextualJMLConstruct> methodlevel_element(ImmutableList<java.lang.String> mods) throws SLTranslationException, org.antlr.runtime.RecognitionException
SLTranslationException
org.antlr.runtime.RecognitionException
public final ImmutableList<java.lang.String> modifiers() throws SLTranslationException, org.antlr.runtime.RecognitionException
SLTranslationException
org.antlr.runtime.RecognitionException
public final java.lang.String modifier() throws org.antlr.runtime.RecognitionException
org.antlr.runtime.RecognitionException
public final ImmutableList<TextualJMLConstruct> class_invariant(ImmutableList<java.lang.String> mods) throws SLTranslationException, org.antlr.runtime.RecognitionException
SLTranslationException
org.antlr.runtime.RecognitionException
public final java.lang.String axiom_name() throws SLTranslationException, org.antlr.runtime.RecognitionException
SLTranslationException
org.antlr.runtime.RecognitionException
public final void invariant_keyword() throws org.antlr.runtime.RecognitionException
org.antlr.runtime.RecognitionException
public final ImmutableList<TextualJMLConstruct> class_axiom(ImmutableList<java.lang.String> mods) throws SLTranslationException, org.antlr.runtime.RecognitionException
SLTranslationException
org.antlr.runtime.RecognitionException
public final ImmutableList<TextualJMLConstruct> initially_clause(ImmutableList<java.lang.String> mods) throws SLTranslationException, org.antlr.runtime.RecognitionException
SLTranslationException
org.antlr.runtime.RecognitionException
public final ImmutableList<TextualJMLConstruct> method_specification(ImmutableList<java.lang.String> mods) throws SLTranslationException, org.antlr.runtime.RecognitionException
SLTranslationException
org.antlr.runtime.RecognitionException
public final void also_keyword() throws org.antlr.runtime.RecognitionException
org.antlr.runtime.RecognitionException
public final ImmutableList<TextualJMLConstruct> spec_case(ImmutableList<java.lang.String> mods) throws SLTranslationException, org.antlr.runtime.RecognitionException
SLTranslationException
org.antlr.runtime.RecognitionException
public final ImmutableList<TextualJMLConstruct> lightweight_spec_case(ImmutableList<java.lang.String> mods) throws SLTranslationException, org.antlr.runtime.RecognitionException
SLTranslationException
org.antlr.runtime.RecognitionException
public final ImmutableList<TextualJMLConstruct> heavyweight_spec_case(ImmutableList<java.lang.String> mods) throws SLTranslationException, org.antlr.runtime.RecognitionException
SLTranslationException
org.antlr.runtime.RecognitionException
public final ImmutableList<TextualJMLConstruct> behavior_spec_case(ImmutableList<java.lang.String> mods) throws SLTranslationException, org.antlr.runtime.RecognitionException
SLTranslationException
org.antlr.runtime.RecognitionException
public final void behavior_keyword() throws org.antlr.runtime.RecognitionException
org.antlr.runtime.RecognitionException
public final ImmutableList<TextualJMLConstruct> normal_behavior_spec_case(ImmutableList<java.lang.String> mods) throws SLTranslationException, org.antlr.runtime.RecognitionException
SLTranslationException
org.antlr.runtime.RecognitionException
public final void normal_behavior_keyword() throws org.antlr.runtime.RecognitionException
org.antlr.runtime.RecognitionException
public final ImmutableList<TextualJMLConstruct> model_behavior_spec_case(ImmutableList<java.lang.String> mods) throws SLTranslationException, org.antlr.runtime.RecognitionException
SLTranslationException
org.antlr.runtime.RecognitionException
public final void model_behavior_keyword() throws org.antlr.runtime.RecognitionException
org.antlr.runtime.RecognitionException
public final ImmutableList<TextualJMLConstruct> exceptional_behavior_spec_case(ImmutableList<java.lang.String> mods) throws SLTranslationException, org.antlr.runtime.RecognitionException
SLTranslationException
org.antlr.runtime.RecognitionException
public final void exceptional_behavior_keyword() throws org.antlr.runtime.RecognitionException
org.antlr.runtime.RecognitionException
public final ImmutableList<TextualJMLConstruct> generic_spec_case(ImmutableList<java.lang.String> mods, Behavior b) throws SLTranslationException, org.antlr.runtime.RecognitionException
SLTranslationException
org.antlr.runtime.RecognitionException
public final ImmutableList<PositionedString[]> spec_var_decls() throws SLTranslationException, org.antlr.runtime.RecognitionException
SLTranslationException
org.antlr.runtime.RecognitionException
public final ImmutableList<PositionedString> spec_header() throws SLTranslationException, org.antlr.runtime.RecognitionException
SLTranslationException
org.antlr.runtime.RecognitionException
public final ImmutableList<PositionedString> free_spec_header() throws SLTranslationException, org.antlr.runtime.RecognitionException
SLTranslationException
org.antlr.runtime.RecognitionException
public final PositionedString requires_clause() throws SLTranslationException, org.antlr.runtime.RecognitionException
SLTranslationException
org.antlr.runtime.RecognitionException
public final void requires_keyword() throws org.antlr.runtime.RecognitionException
org.antlr.runtime.RecognitionException
public final PositionedString requires_free_clause() throws SLTranslationException, org.antlr.runtime.RecognitionException
SLTranslationException
org.antlr.runtime.RecognitionException
public final ImmutableList<TextualJMLConstruct> generic_spec_body(ImmutableList<java.lang.String> mods, Behavior b, ImmutableList<TextualJMLConstruct> specs) throws SLTranslationException, org.antlr.runtime.RecognitionException
SLTranslationException
org.antlr.runtime.RecognitionException
public final ImmutableList<TextualJMLConstruct> generic_spec_case_seq(ImmutableList<java.lang.String> mods, Behavior b, ImmutableList<TextualJMLConstruct> specs) throws SLTranslationException, org.antlr.runtime.RecognitionException
SLTranslationException
org.antlr.runtime.RecognitionException
public final ImmutableList<TextualJMLConstruct> simple_spec_body(ImmutableList<java.lang.String> mods, Behavior b) throws SLTranslationException, org.antlr.runtime.RecognitionException
SLTranslationException
org.antlr.runtime.RecognitionException
public final void simple_spec_body_clause(TextualJMLSpecCase sc, Behavior b) throws SLTranslationException, org.antlr.runtime.RecognitionException
SLTranslationException
org.antlr.runtime.RecognitionException
public final PositionedString separates_clause() throws SLTranslationException, org.antlr.runtime.RecognitionException
SLTranslationException
org.antlr.runtime.RecognitionException
public final void separates_keyword() throws org.antlr.runtime.RecognitionException
org.antlr.runtime.RecognitionException
public final PositionedString determines_clause() throws SLTranslationException, org.antlr.runtime.RecognitionException
SLTranslationException
org.antlr.runtime.RecognitionException
public final void determines_keyword() throws org.antlr.runtime.RecognitionException
org.antlr.runtime.RecognitionException
public final PositionedString assignable_clause() throws SLTranslationException, org.antlr.runtime.RecognitionException
SLTranslationException
org.antlr.runtime.RecognitionException
public final void assignable_keyword() throws org.antlr.runtime.RecognitionException
org.antlr.runtime.RecognitionException
public final PositionedString accessible_clause() throws SLTranslationException, org.antlr.runtime.RecognitionException
SLTranslationException
org.antlr.runtime.RecognitionException
public final void accessible_keyword() throws org.antlr.runtime.RecognitionException
org.antlr.runtime.RecognitionException
public final PositionedString measured_by_clause() throws SLTranslationException, org.antlr.runtime.RecognitionException
SLTranslationException
org.antlr.runtime.RecognitionException
public final void measured_by_keyword() throws org.antlr.runtime.RecognitionException
org.antlr.runtime.RecognitionException
public final PositionedString ensures_clause() throws SLTranslationException, org.antlr.runtime.RecognitionException
SLTranslationException
org.antlr.runtime.RecognitionException
public final void ensures_keyword() throws org.antlr.runtime.RecognitionException
org.antlr.runtime.RecognitionException
public final PositionedString ensures_free_clause() throws SLTranslationException, org.antlr.runtime.RecognitionException
SLTranslationException
org.antlr.runtime.RecognitionException
public final PositionedString signals_clause() throws SLTranslationException, org.antlr.runtime.RecognitionException
SLTranslationException
org.antlr.runtime.RecognitionException
public final void signals_keyword() throws org.antlr.runtime.RecognitionException
org.antlr.runtime.RecognitionException
public final PositionedString signals_only_clause() throws SLTranslationException, org.antlr.runtime.RecognitionException
SLTranslationException
org.antlr.runtime.RecognitionException
public final void signals_only_keyword() throws org.antlr.runtime.RecognitionException
org.antlr.runtime.RecognitionException
public final PositionedString diverges_clause() throws SLTranslationException, org.antlr.runtime.RecognitionException
SLTranslationException
org.antlr.runtime.RecognitionException
public final void diverges_keyword() throws org.antlr.runtime.RecognitionException
org.antlr.runtime.RecognitionException
public final void captures_clause() throws SLTranslationException, org.antlr.runtime.RecognitionException
SLTranslationException
org.antlr.runtime.RecognitionException
public final void captures_keyword() throws org.antlr.runtime.RecognitionException
org.antlr.runtime.RecognitionException
public final PositionedString name_clause() throws SLTranslationException, org.antlr.runtime.RecognitionException
SLTranslationException
org.antlr.runtime.RecognitionException
public final void when_clause() throws SLTranslationException, org.antlr.runtime.RecognitionException
SLTranslationException
org.antlr.runtime.RecognitionException
public final void when_keyword() throws org.antlr.runtime.RecognitionException
org.antlr.runtime.RecognitionException
public final void working_space_clause() throws SLTranslationException, org.antlr.runtime.RecognitionException
SLTranslationException
org.antlr.runtime.RecognitionException
public final void working_space_keyword() throws org.antlr.runtime.RecognitionException
org.antlr.runtime.RecognitionException
public final void duration_clause() throws SLTranslationException, org.antlr.runtime.RecognitionException
SLTranslationException
org.antlr.runtime.RecognitionException
public final void duration_keyword() throws org.antlr.runtime.RecognitionException
org.antlr.runtime.RecognitionException
public final PositionedString[] old_clause() throws SLTranslationException, org.antlr.runtime.RecognitionException
SLTranslationException
org.antlr.runtime.RecognitionException
public final PositionedString type() throws org.antlr.runtime.RecognitionException
org.antlr.runtime.RecognitionException
public final ImmutableList<TextualJMLConstruct> field_or_method_declaration(ImmutableList<java.lang.String> mods) throws org.antlr.runtime.RecognitionException
org.antlr.runtime.RecognitionException
public final ImmutableList<TextualJMLConstruct> field_declaration(ImmutableList<java.lang.String> mods, PositionedString type, org.antlr.runtime.Token name) throws org.antlr.runtime.RecognitionException
org.antlr.runtime.RecognitionException
public final ImmutableList<TextualJMLConstruct> method_declaration(ImmutableList<java.lang.String> mods, PositionedString type, org.antlr.runtime.Token name) throws org.antlr.runtime.RecognitionException
org.antlr.runtime.RecognitionException
public final java.lang.String param_list() throws org.antlr.runtime.RecognitionException
org.antlr.runtime.RecognitionException
public final java.lang.String param_decl() throws org.antlr.runtime.RecognitionException
org.antlr.runtime.RecognitionException
public final ImmutableList<TextualJMLConstruct> represents_clause(ImmutableList<java.lang.String> mods) throws SLTranslationException, org.antlr.runtime.RecognitionException
SLTranslationException
org.antlr.runtime.RecognitionException
public final void represents_keyword() throws org.antlr.runtime.RecognitionException
org.antlr.runtime.RecognitionException
public final ImmutableList<TextualJMLConstruct> depends_clause(ImmutableList<java.lang.String> mods) throws SLTranslationException, org.antlr.runtime.RecognitionException
SLTranslationException
org.antlr.runtime.RecognitionException
public final ImmutableList<TextualJMLConstruct> history_constraint(ImmutableList<java.lang.String> mods) throws SLTranslationException, org.antlr.runtime.RecognitionException
SLTranslationException
org.antlr.runtime.RecognitionException
public final void constraint_keyword() throws org.antlr.runtime.RecognitionException
org.antlr.runtime.RecognitionException
public final ImmutableList<TextualJMLConstruct> monitors_for_clause(ImmutableList<java.lang.String> mods) throws SLTranslationException, org.antlr.runtime.RecognitionException
SLTranslationException
org.antlr.runtime.RecognitionException
public final ImmutableList<TextualJMLConstruct> readable_if_clause(ImmutableList<java.lang.String> mods) throws SLTranslationException, org.antlr.runtime.RecognitionException
SLTranslationException
org.antlr.runtime.RecognitionException
public final ImmutableList<TextualJMLConstruct> writable_if_clause(ImmutableList<java.lang.String> mods) throws SLTranslationException, org.antlr.runtime.RecognitionException
SLTranslationException
org.antlr.runtime.RecognitionException
public final ImmutableList<TextualJMLConstruct> datagroup_clause(ImmutableList<java.lang.String> mods) throws SLTranslationException, org.antlr.runtime.RecognitionException
SLTranslationException
org.antlr.runtime.RecognitionException
public final void in_group_clause() throws SLTranslationException, org.antlr.runtime.RecognitionException
SLTranslationException
org.antlr.runtime.RecognitionException
public final void in_keyword() throws org.antlr.runtime.RecognitionException
org.antlr.runtime.RecognitionException
public final void maps_into_clause() throws SLTranslationException, org.antlr.runtime.RecognitionException
SLTranslationException
org.antlr.runtime.RecognitionException
public final void maps_keyword() throws org.antlr.runtime.RecognitionException
org.antlr.runtime.RecognitionException
public final ImmutableList<TextualJMLConstruct> nowarn_pragma(ImmutableList<java.lang.String> mods) throws SLTranslationException, org.antlr.runtime.RecognitionException
SLTranslationException
org.antlr.runtime.RecognitionException
public final ImmutableList<TextualJMLConstruct> debug_statement(ImmutableList<java.lang.String> mods) throws SLTranslationException, org.antlr.runtime.RecognitionException
SLTranslationException
org.antlr.runtime.RecognitionException
public final ImmutableList<TextualJMLConstruct> set_statement(ImmutableList<java.lang.String> mods) throws org.antlr.runtime.RecognitionException
org.antlr.runtime.RecognitionException
public final ImmutableList<TextualJMLConstruct> merge_point_statement(ImmutableList<java.lang.String> mods) throws org.antlr.runtime.RecognitionException
org.antlr.runtime.RecognitionException
public final ImmutableList<TextualJMLConstruct> loop_specification(ImmutableList<java.lang.String> mods) throws SLTranslationException, org.antlr.runtime.RecognitionException
SLTranslationException
org.antlr.runtime.RecognitionException
public final PositionedString loop_invariant() throws org.antlr.runtime.RecognitionException
org.antlr.runtime.RecognitionException
public final PositionedString loop_invariant_free() throws org.antlr.runtime.RecognitionException
org.antlr.runtime.RecognitionException
public final void maintaining_keyword() throws org.antlr.runtime.RecognitionException
org.antlr.runtime.RecognitionException
public final PositionedString variant_function() throws org.antlr.runtime.RecognitionException
org.antlr.runtime.RecognitionException
public final void decreasing_keyword() throws org.antlr.runtime.RecognitionException
org.antlr.runtime.RecognitionException
public final PositionedString loop_separates_clause() throws SLTranslationException, org.antlr.runtime.RecognitionException
SLTranslationException
org.antlr.runtime.RecognitionException
public final PositionedString loop_determines_clause() throws SLTranslationException, org.antlr.runtime.RecognitionException
SLTranslationException
org.antlr.runtime.RecognitionException
public final ImmutableList<TextualJMLConstruct> assume_statement(ImmutableList<java.lang.String> mods) throws SLTranslationException, org.antlr.runtime.RecognitionException
SLTranslationException
org.antlr.runtime.RecognitionException
public final void assume_keyword() throws org.antlr.runtime.RecognitionException
org.antlr.runtime.RecognitionException
public final PositionedString expression() throws org.antlr.runtime.RecognitionException
org.antlr.runtime.RecognitionException
public final java.lang.String initialiser() throws org.antlr.runtime.RecognitionException
org.antlr.runtime.RecognitionException
public final ImmutableList<TextualJMLConstruct> block_specification(ImmutableList<java.lang.String> mods) throws SLTranslationException, org.antlr.runtime.RecognitionException
SLTranslationException
org.antlr.runtime.RecognitionException
public final ImmutableList<TextualJMLConstruct> block_loop_specification(ImmutableList<java.lang.String> mods) throws SLTranslationException, org.antlr.runtime.RecognitionException
SLTranslationException
org.antlr.runtime.RecognitionException
public final void loop_contract_keyword() throws org.antlr.runtime.RecognitionException
org.antlr.runtime.RecognitionException
public final ImmutableList<TextualJMLConstruct> assert_statement(ImmutableList<java.lang.String> mods) throws SLTranslationException, org.antlr.runtime.RecognitionException
SLTranslationException
org.antlr.runtime.RecognitionException
public final void assert_keyword() throws org.antlr.runtime.RecognitionException
org.antlr.runtime.RecognitionException
public final PositionedString breaks_clause() throws SLTranslationException, org.antlr.runtime.RecognitionException
SLTranslationException
org.antlr.runtime.RecognitionException
public final void breaks_keyword() throws org.antlr.runtime.RecognitionException
org.antlr.runtime.RecognitionException
public final PositionedString continues_clause() throws SLTranslationException, org.antlr.runtime.RecognitionException
SLTranslationException
org.antlr.runtime.RecognitionException
public final void continues_keyword() throws org.antlr.runtime.RecognitionException
org.antlr.runtime.RecognitionException
public final PositionedString returns_clause() throws SLTranslationException, org.antlr.runtime.RecognitionException
SLTranslationException
org.antlr.runtime.RecognitionException
public final void returns_keyword() throws org.antlr.runtime.RecognitionException
org.antlr.runtime.RecognitionException
public final ImmutableList<TextualJMLConstruct> break_behavior_spec_case(ImmutableList<java.lang.String> mods) throws SLTranslationException, org.antlr.runtime.RecognitionException
SLTranslationException
org.antlr.runtime.RecognitionException
public final void break_behavior_keyword() throws org.antlr.runtime.RecognitionException
org.antlr.runtime.RecognitionException
public final ImmutableList<TextualJMLConstruct> continue_behavior_spec_case(ImmutableList<java.lang.String> mods) throws SLTranslationException, org.antlr.runtime.RecognitionException
SLTranslationException
org.antlr.runtime.RecognitionException
public final void continue_behavior_keyword() throws org.antlr.runtime.RecognitionException
org.antlr.runtime.RecognitionException
public final ImmutableList<TextualJMLConstruct> return_behavior_spec_case(ImmutableList<java.lang.String> mods) throws SLTranslationException, org.antlr.runtime.RecognitionException
SLTranslationException
org.antlr.runtime.RecognitionException
public final void return_behavior_keyword() throws org.antlr.runtime.RecognitionException
org.antlr.runtime.RecognitionException
public final void synpred1_KeYJMLPreParser_fragment() throws org.antlr.runtime.RecognitionException
org.antlr.runtime.RecognitionException
public final void synpred2_KeYJMLPreParser_fragment() throws org.antlr.runtime.RecognitionException
org.antlr.runtime.RecognitionException
public final boolean synpred2_KeYJMLPreParser()
public final boolean synpred1_KeYJMLPreParser()