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.
|
| IntermediatePresentationProofFileParser.BuiltinRuleInformation |
Information about built-in rule applications.
|
| IntermediatePresentationProofFileParser.Result |
Simple structure comprising the results of the parser.
|
| IntermediatePresentationProofFileParser.RuleInformation |
General information about taclet and built-in rule applications.
|
| IntermediatePresentationProofFileParser.TacletInformation |
Information about taclet applications.
|
| IntermediateProofReplayer |
This class is responsible for generating a KeY proof from an intermediate
representation generated by
IntermediatePresentationProofFileParser. |
| IntermediateProofReplayer.Result |
Simple structure containing the results of the replay procedure.
|
| 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. |
| 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 |
|---|---|
| IntermediateProofReplayer.BuiltInConstructionException |
Signals an error during construction of a built-in rule app.
|
| IntermediateProofReplayer.SkipSMTRuleException |
Signals that the execution of an SMT solver, that has been used before
the now loaded proof was saved, has been skipped.
|
| IntermediateProofReplayer.TacletConstructionException |
Signals an error during construction of a taclet app.
|
| ProblemLoaderException |