Package | Description |
---|---|
de.uka.ilkd.key.control | |
de.uka.ilkd.key.control.instantiation_model | |
de.uka.ilkd.key.core | |
de.uka.ilkd.key.gui |
This package contains classes forming the graphical user interface of KeY.
|
de.uka.ilkd.key.gui.extension.api | |
de.uka.ilkd.key.gui.extension.impl | |
de.uka.ilkd.key.gui.nodeviews | |
de.uka.ilkd.key.gui.originlabels | |
de.uka.ilkd.key.gui.utilities | |
de.uka.ilkd.key.java |
This package contains classes that cover the Java programming language.
|
de.uka.ilkd.key.logic.label | |
de.uka.ilkd.key.macros.scripts |
Proof script commands are a simple proof automation facility.
|
de.uka.ilkd.key.nparser | |
de.uka.ilkd.key.nparser.builder | |
de.uka.ilkd.key.parser |
This package contains the parser for .key and .proof files.
|
de.uka.ilkd.key.pp |
This package contains pretty-printing functionality used by the GUI and for
saving proofs.
|
de.uka.ilkd.key.proof |
This package contains the core data structures of proofs, nodes, goals, as well
as machinery to deal with these data structures.
|
de.uka.ilkd.key.symbolic_execution.util | |
org.key_project.exploration.actions |
Class and Description |
---|
VisibleTermLabels
This abstract class is used by SequentViewLogicPrinter to determine the set
of printed TermLabels.
|
Class and Description |
---|
AbbrevMap |
Class and Description |
---|
NotationInfo
Stores the mapping from operators to
Notation s. |
Class and Description |
---|
LogicPrinter
The front end for the Sequent pretty-printer.
|
Class and Description |
---|
PosInSequent
describes a position in a sequent including the bounds within a string
representation of the sequent.
|
Class and Description |
---|
PosInSequent
describes a position in a sequent including the bounds within a string
representation of the sequent.
|
Class and Description |
---|
NotationInfo
Stores the mapping from operators to
Notation s. |
PosInSequent
describes a position in a sequent including the bounds within a string
representation of the sequent.
|
Range
A class specifying a range of integer numbers e.g.
|
SequentPrintFilter
Filter a given sequent to prepare it for the SequentPrinter class
by adjusting constraints, deleting formulas, etc.
|
SequentViewLogicPrinter
Subclass of
LogicPrinter used in GUI. |
VisibleTermLabels
This abstract class is used by SequentViewLogicPrinter to determine the set
of printed TermLabels.
|
Class and Description |
---|
PosInSequent
describes a position in a sequent including the bounds within a string
representation of the sequent.
|
Class and Description |
---|
PosInSequent
describes a position in a sequent including the bounds within a string
representation of the sequent.
|
Class and Description |
---|
Range
A class specifying a range of integer numbers e.g.
|
Class and Description |
---|
PosInSequent
describes a position in a sequent including the bounds within a string
representation of the sequent.
|
Class and Description |
---|
AbbrevMap |
Class and Description |
---|
AbbrevMap |
Class and Description |
---|
AbbrevMap |
Class and Description |
---|
AbbrevMap |
Class and Description |
---|
AbbrevException |
AbbrevMap |
AbbrevMap.AbbrevWrapper |
IllegalRegexException
This exception is thrown when a String is expected be a valid
regular expression, but is not.
|
InitialPositionTable
An InitialPositionTable is a PositionTable that describes the
beginning of the element/subelement relationship.
|
LogicPrinter
The front end for the Sequent pretty-printer.
|
Notation
Encapsulate the concrete syntax used to print a term.
|
Notation.HeapConstructorNotation
The standard concrete syntax for heap constructors.
|
Notation.VariableNotation
The standard concrete syntax for all kinds of variables.
|
NotationInfo
Stores the mapping from operators to
Notation s. |
PosInSequent
describes a position in a sequent including the bounds within a string
representation of the sequent.
|
PositionTable
A PositionTable describes the start and end positions of substrings of a
String in order to get a PosInSequent from an int describing a position in a
string representing a Term or a Sequent, etc.
|
ProgramPrinter |
Range
A class specifying a range of integer numbers e.g.
|
SearchSequentPrintFilter
This is an interface for filters that are used to
modify the sequent view, improving the search function.
|
SequentPrintFilter
Filter a given sequent to prepare it for the SequentPrinter class
by adjusting constraints, deleting formulas, etc.
|
SequentPrintFilterEntry
One element of a sequent as delivered by SequentPrintFilter
|
SequentViewLogicPrinter
Subclass of
LogicPrinter used in GUI. |
VisibleTermLabels
This abstract class is used by SequentViewLogicPrinter to determine the set
of printed TermLabels.
|
Class and Description |
---|
AbbrevMap |
Class and Description |
---|
NotationInfo
Stores the mapping from operators to
Notation s. |
Class and Description |
---|
PosInSequent
describes a position in a sequent including the bounds within a string
representation of the sequent.
|
Copyright © 2003-2019 The KeY-Project.