Package | Description |
---|---|
de.uka.ilkd.key.api |
This package gives an high-level entry point to the KeY world.
|
de.uka.ilkd.key.control | |
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.nparser | |
de.uka.ilkd.key.proof.init |
This package contains classes handling prover initialisation.
|
de.uka.ilkd.key.proof.io |
Classes related to loading and saving proof files.
|
de.uka.ilkd.key.proof.io.consistency | |
de.uka.ilkd.key.proof.io.event | |
de.uka.ilkd.key.speclang |
This package contains the specification language frontends of KeY.
|
de.uka.ilkd.key.taclettranslation.lemma | |
de.uka.ilkd.key.ui | |
de.uka.ilkd.key.util |
This package is a grab bag of miscellaneous useful code fragments.
|
Class and Description |
---|
ProblemLoaderException |
Class and Description |
---|
AbstractProblemLoader
This class provides the basic functionality to load something in KeY.
|
AbstractProblemLoader.ReplayResult |
ProblemLoaderControl
Allows to observe and control the loading performed by an
AbstractProblemLoader . |
ProblemLoaderException |
Class and Description |
---|
AutoSaver
Saves intermediate proof artifacts during strategy execution.
|
Class and Description |
---|
AbstractProblemLoader
This class provides the basic functionality to load something in KeY.
|
AbstractProblemLoader.ReplayResult |
ProblemLoaderControl
Allows to observe and control the loading performed by an
AbstractProblemLoader . |
ProblemLoaderException |
Class and Description |
---|
IProofFileParser
Defines the required which a
KeYParser needs to parse a *.proof file
and to apply the rules again. |
Class and Description |
---|
EnvInput
Represents an entity read to produce an environment to read a proof
obligation.
|
IProofFileParser
Defines the required which a
KeYParser needs to parse a *.proof file
and to apply the rules again. |
KeYFile
Represents an input from a .key file producing an environment.
|
RuleSource |
Class and Description |
---|
AbstractProblemLoader
This class provides the basic functionality to load something in KeY.
|
AbstractProblemLoader.ReplayResult |
AutoSaver
Saves intermediate proof artifacts during strategy execution.
|
EnvInput
Represents an entity read to produce an environment to read a proof
obligation.
|
FileRuleSource |
IProofFileParser
Defines the required which a
KeYParser needs to parse a *.proof file
and to apply the rules again. |
IProofFileParser.ProofElementID
Enumeration of the different syntactic elements occurring in a saved
proof tree representation.
|
KeYFile
Represents an input from a .key file producing an environment.
|
LDTInput.LDTInputListener |
OutputStreamProofSaver
Saves a proof to a given
OutputStream . |
ProblemLoaderControl
Allows to observe and control the loading performed by an
AbstractProblemLoader . |
ProblemLoaderException |
ProofSaver
Saves a proof and provides useful methods for pretty printing
terms or programs.
|
RuleSource |
Class and Description |
---|
RuleSource |
Class and Description |
---|
ProofSaver
Saves a proof and provides useful methods for pretty printing
terms or programs.
|
Class and Description |
---|
AbstractEnvInput
A simple EnvInput which includes default rules and a Java path.
|
EnvInput
Represents an entity read to produce an environment to read a proof
obligation.
|
Class and Description |
---|
AbstractEnvInput
A simple EnvInput which includes default rules and a Java path.
|
EnvInput
Represents an entity read to produce an environment to read a proof
obligation.
|
Class and Description |
---|
ProblemLoader
This class extends the functionality of the
AbstractProblemLoader . |
ProblemLoaderControl
Allows to observe and control the loading performed by an
AbstractProblemLoader . |
Class and Description |
---|
ProblemLoaderException |
Copyright © 2003-2019 The KeY-Project.