See: Description
Interface | 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. |
LDTInput.LDTInputListener | |
ProblemLoaderControl |
Allows to observe and control the loading performed by an
AbstractProblemLoader . |
Class | Description |
---|---|
AbstractEnvInput |
A simple EnvInput which includes default rules and a Java path.
|
AbstractProblemLoader |
This class provides the basic functionality to load something in KeY.
|
AbstractProblemLoader.ReplayResult | |
AutoSaver |
Saves intermediate proof artifacts during strategy execution.
|
CountingBufferedReader | |
FileRuleSource | |
GZipFileRuleSource |
This file rule source derivative wraps its input stream into a
GZIPInputStream thus allowing decompressing gnu-zipped proof files. |
GZipProofSaver |
This proof saver derivative wraps its generated output stream into a
GZIPOutputStream thus compressing proof files. |
IntermediatePresentationProofFileParser |
Parses a KeY proof file into an intermediate representation.
|
IntermediateProofReplayer |
This class is responsible for generating a KeY proof from an intermediate
representation generated by
IntermediatePresentationProofFileParser . |
KeYFile |
Represents an input from a .key file producing an environment.
|
LDTInput |
Represents the LDT .key files as a whole.
|
OutputStreamProofSaver |
Saves a proof to a given
OutputStream . |
ProblemLoader |
This class extends the functionality of the
AbstractProblemLoader . |
ProofBundleSaver |
This class is responsible for saving (zipped) proof bundles.
|
ProofSaver |
Saves a proof and provides useful methods for pretty printing
terms or programs.
|
RuleSource | |
RuleSourceFactory | |
SingleThreadProblemLoader |
This single threaded problem loader is used by the Eclipse integration of KeY.
|
UrlRuleSource |
Enum | Description |
---|---|
IProofFileParser.ProofElementID |
Enumeration of the different syntactic elements occurring in a saved
proof tree representation.
|
Exception | Description |
---|---|
ProblemLoaderException |
Copyright © 2003-2019 The KeY-Project.