ChoiceInformation |
A POJO representing the information on choices in ASTs.
|
DebugKeyLexer |
This program is a little for debugging KeY Lexer.
|
KeyAst<T extends org.antlr.v4.runtime.ParserRuleContext> |
This is a monad around the parse tree.
|
KeyAst.File |
|
KeyAst.Seq |
|
KeyAst.Term |
|
KeyIO |
This facade provides high level access to parse and
interpret key files or input strings into declarations, proof, problem, terms.
|
KeYLexer |
|
KeYParser |
|
KeYParser.AbbreviationContext |
|
KeYParser.AccesstermContext |
|
KeYParser.Activated_choiceContext |
|
KeYParser.AddContext |
|
KeYParser.AddprogvarContext |
|
KeYParser.AddrulesContext |
|
KeYParser.Arg_sorts_or_formula_helperContext |
|
KeYParser.Arg_sorts_or_formulaContext |
|
KeYParser.Arg_sortsContext |
|
KeYParser.Argument_listContext |
|
KeYParser.ArrayopidContext |
|
KeYParser.Atom_prefixContext |
|
KeYParser.Attribute_complexContext |
|
KeYParser.Attribute_simpleContext |
|
KeYParser.Attribute_starContext |
|
KeYParser.AttributeContext |
|
KeYParser.Boolean_literalContext |
|
KeYParser.BootClassPathContext |
|
KeYParser.Bound_variablesContext |
|
KeYParser.Brace_suffixContext |
|
KeYParser.Bracket_access_heap_termContext |
|
KeYParser.Bracket_access_heap_updateContext |
|
KeYParser.Bracket_access_indexrangeContext |
|
KeYParser.Bracket_access_starContext |
|
KeYParser.Bracket_suffix_heapContext |
|
KeYParser.Bracket_termContext |
|
KeYParser.CallContext |
|
KeYParser.Cast_termContext |
|
KeYParser.Char_literalContext |
|
KeYParser.ChoiceContext |
|
KeYParser.ClassPathsContext |
|
KeYParser.Comparison_termContext |
|
KeYParser.Conjunction_termContext |
|
KeYParser.ContractsContext |
|
KeYParser.DeclsContext |
|
KeYParser.Disjunction_termContext |
|
KeYParser.Elementary_update_termContext |
|
KeYParser.Equality_termContext |
|
KeYParser.Equivalence_termContext |
|
KeYParser.Extends_sortsContext |
|
KeYParser.FileContext |
|
KeYParser.Func_declContext |
|
KeYParser.Func_declsContext |
|
KeYParser.Funcpred_nameContext |
|
KeYParser.GoalspecContext |
|
KeYParser.GoalspecsContext |
|
KeYParser.GoalspecwithoptionContext |
|
KeYParser.Id_declarationContext |
|
KeYParser.IfExThenElseTermContext |
|
KeYParser.IfThenElseTermContext |
|
KeYParser.Implication_termContext |
|
KeYParser.InvariantsContext |
|
KeYParser.JavaSourceContext |
|
KeYParser.KeyjavatypeContext |
|
KeYParser.LabelContext |
|
KeYParser.LiteralsContext |
|
KeYParser.Location_termContext |
|
KeYParser.Locset_termContext |
|
KeYParser.MetaIdContext |
|
KeYParser.MetaTermContext |
|
KeYParser.Modality_termContext |
|
KeYParser.ModifiersContext |
|
KeYParser.Negation_termContext |
|
KeYParser.NumberContext |
|
KeYParser.One_bound_variableContext |
|
KeYParser.One_contractContext |
|
KeYParser.One_include_statementContext |
|
KeYParser.One_includeContext |
|
KeYParser.One_invariantContext |
|
KeYParser.One_schema_modal_op_declContext |
|
KeYParser.One_schema_var_declContext |
|
KeYParser.One_sort_declContext |
|
KeYParser.OneJavaSourceContext |
|
KeYParser.Oneof_sortsContext |
|
KeYParser.Option_declsContext |
|
KeYParser.Option_listContext |
|
KeYParser.OptionContext |
|
KeYParser.OptionDeclContext |
|
KeYParser.Options_choiceContext |
|
KeYParser.Parallel_termContext |
|
KeYParser.Pred_declContext |
|
KeYParser.Pred_declsContext |
|
KeYParser.PreferencesContext |
|
KeYParser.Primitive_labeled_termContext |
|
KeYParser.Primitive_termContext |
|
KeYParser.ProblemContext |
|
KeYParser.ProfileContext |
|
KeYParser.Prog_var_declsContext |
|
KeYParser.ProofContext |
|
KeYParser.ProofScriptContext |
|
KeYParser.PvsetContext |
|
KeYParser.QuantifiertermContext |
|
KeYParser.ReplacewithContext |
|
KeYParser.Ruleset_declsContext |
|
KeYParser.RulesetContext |
|
KeYParser.RulesetsContext |
|
KeYParser.RulesOrAxiomsContext |
|
KeYParser.Schema_modifiersContext |
|
KeYParser.Schema_var_declsContext |
|
KeYParser.SemisequentContext |
|
KeYParser.SeqContext |
|
KeYParser.SeqEOFContext |
|
KeYParser.Simple_ident_comma_listContext |
|
KeYParser.Simple_ident_dots_comma_listContext |
|
KeYParser.Simple_ident_dotsContext |
|
KeYParser.Simple_identContext |
|
KeYParser.Single_labelContext |
|
KeYParser.Sort_declsContext |
|
KeYParser.SortIdContext |
|
KeYParser.String_literalContext |
|
KeYParser.String_valueContext |
|
KeYParser.Strong_arith_term_1Context |
|
KeYParser.Strong_arith_term_2Context |
|
KeYParser.Substitution_termContext |
|
KeYParser.TacletContext |
|
KeYParser.TacletlistContext |
|
KeYParser.Term60Context |
|
KeYParser.TermContext |
|
KeYParser.TermEOFContext |
|
KeYParser.TermorseqContext |
|
KeYParser.TermParenContext |
|
KeYParser.Transform_declContext |
|
KeYParser.Transform_declsContext |
|
KeYParser.TriggersContext |
|
KeYParser.Unary_formulaContext |
|
KeYParser.Unary_minus_termContext |
|
KeYParser.Update_termContext |
|
KeYParser.Varexp_argumentContext |
|
KeYParser.VarexpContext |
|
KeYParser.VarexpIdContext |
|
KeYParser.VarexplistContext |
|
KeYParser.VarIdContext |
|
KeYParser.VarIdsContext |
|
KeYParser.Weak_arith_termContext |
|
KeYParser.Where_to_bindContext |
|
KeYParserBaseListener |
This class provides an empty implementation of KeYParserListener ,
which can be extended to create a listener which only needs to handle a subset
of the available methods.
|
KeYParserBaseVisitor<T> |
This class provides an empty implementation of KeYParserVisitor ,
which can be extended to create a visitor which only needs to handle a subset
of the available methods.
|
ParsingFacade |
This facade provides low-level access to the ANTLR4 Parser and Lexer.
|
ProblemInformation |
This POJO represents the static information of a KeY problem.
|
ProofReplayer |
A short little hack, but completely working and fast, for replaying proofs inside KeY files.
|