See: Description
Interface | Description |
---|---|
ApplyStrategy.IStopCondition |
Implementation of this interface are used in
ApplyStrategy to
determine if the strategy should stop or continue. |
GoalChooserBuilder |
interface to be implemented by builders returning a
goal chooser
|
GoalListener |
interface to be implemented by a goal listener
|
IGoalChooser |
Interface to be implemented by classes in order to customize the goal selection
strategy of the automatic prover environment.
|
InstantiationProposer |
Provides proposals for schema variable instantiations.
|
ITermTacletAppIndexCache |
The general interface for caches for accelerating
TermTacletAppIndex . |
ModelChangeListener |
this interface is implemented by listener of change
events of a model
|
NewRuleListener |
Interface for tracking new RuleApps
|
ProofTreeListener | |
ProofVisitor | |
ProverTaskListener |
Listener for longer tasks, which may be run in a separate worker thread.
|
RuleAppListener | |
StrategyInfoUndoMethod | |
TaskFinishedInfo |
An information object with additional information about the
finished task.
|
TaskStartedInfo |
Used as an event object to inform about a prover task
that is just about to start.
|
Class | Description |
---|---|
ApplyStrategy |
Applies rules in an automated fashion.
|
ApplyStrategy.AppliedRuleStopCondition |
Implementation of
ApplyStrategy.IStopCondition which stops the strategy
after a reached limit of rules or after a timeout in ms. |
ApplyStrategy.ApplyStrategyInfo |
The final result of the strategy application is stored in this container
and returned to the instance that started the strategies.
|
ApplyStrategy.SingleRuleApplicationInfo |
Instances of this class are used to store if a rule could be applied automatically and if not
to store the reason why no rule applications could be performed.
|
BuiltInRuleAppIndex | |
BuiltInRuleIndex |
Index for managing built-in-rules usch as integer decision or update
simplification rule.
|
CompoundProof | |
Counter |
Proof-specific counter object: taclet names, var names, node numbers, &c
|
DefaultGoalChooser |
Helper class for managing a list of goals on which rules are applied.
|
DefaultGoalChooserBuilder |
creates the default goal chooser used in KeY
|
DefaultTaskFinishedInfo | |
DefaultTaskStartedInfo |
Default implementation of a
TaskStartedInfo . |
DepthFirstGoalChooser |
Helper class for managing a list of goals on which rules are applied.
|
DepthFirstGoalChooserBuilder | |
FormulaTag |
Class whose instances represent tags to identify the formulas of sequents
persistently, i.e. a tag does not become invalid when a formula is modified
by a rule application.
|
FormulaTagManager |
Class to manage the tags of the formulas of a sequent (node).
|
FormulaTagManager.FormulaInfo |
Class that holds information about a formula, namely the current position
(
PosInOccurrence ) as well as a list of the modifications
that have been applied to the formula so far. |
Goal |
A proof is represented as a tree of nodes containing sequents.
|
InstantiationProposerCollection |
Composite of instantiation proposers.
|
JavaModel | |
ModelEvent |
this class represents a Model event
|
MultiThreadedTacletIndex |
A multi-threaded taclet index implementation.
|
MultiThreadedTacletIndex.TacletSetMatchTask |
The callable implementing the actual matching task.
|
NameRecorder | |
Node | |
NodeInfo |
The node info object contains additional information about a node used to
give user feedback.
|
NodeIterator | |
NullNewRuleListener |
Implementation of the NewRuleListener interface
that does nothing
|
ObserverWithType | |
OpReplacer |
Replaces operators in a term by other operators with the same signature,
or subterms of the term by other terms with the same sort.
|
PrefixTermTacletAppIndexCache |
The abstract superclass of caches for taclet app indexes that are separated
by different prefixes of bound variables.
|
PrefixTermTacletAppIndexCacheImpl |
The abstract superclass of caches for taclet app indexes that are implemented
using a common backend
LRUCache (the backend is stored in
TermTacletAppIndexCacheSet ). |
PrefixTermTacletAppIndexCacheImpl.CacheKey | |
ProgVarReplacer |
Replaces program variables.
|
Proof |
A proof is represented as a tree whose nodes are created by
applying rules on the current (open) goals and dividing them up
into several new subgoals.
|
ProofAggregate | |
ProofEvent |
an object indicating that a proof event has happpend
|
ProofTreeAdapter |
An abstract adapter class for receiving proof tree events.
|
ProofTreeEvent |
Encapsulates information describing changes to a proof tree, and
used to notify proof tree listeners of the change.
|
RuleAppIndex |
manages the possible application of rules (RuleApps)
|
SemisequentTacletAppIndex |
This class holds
TermTacletAppIndex s for all formulas of
a semisequent. |
SingleProof | |
SingleThreadedTacletIndex |
The default taclet index implementation.
|
Statistics |
Instances of this class encapsulate statistical information about proofs,
such as the number of nodes, or the number of interactions.
|
SubtreeIterator |
Iterator over subtree.
|
TacletAppIndex |
the class manages the available TacletApps.
|
TacletIndex |
manages all applicable Taclets (more precisely: Taclets with
instantiations but without position information, the NoPosTacletApps)
at one node.
|
TacletIndex.PrefixOccurrences |
Inner class to track the occurrences of prefix elements in java blocks
|
TacletIndexKit |
Abstract factory for creating
TacletIndex instances |
TacletIndexKit.MultiThreadedTacletIndexKit |
Concrete factory creating the multi threaded version of the
TacletIndex
(performs matching using multiple threads) |
TacletIndexKit.SingleThreadedTacletIndexKit |
Concrete factory creating the single threaded version of the
TacletIndex |
TermProgramVariableCollector | |
TermProgramVariableCollectorKeepUpdatesForBreakpointconditions | |
TermTacletAppIndex |
Class whose objects represent an index of taclet apps for one particular
position within a formula, and that also contain references to the indices of
direct subformulas
|
TermTacletAppIndexCacheSet |
Cache that is used for accelerating
TermTacletAppIndex . |
VariableNameProposer |
Proposes names for variables (except program variables).
|
Enum | Description |
---|---|
TaskStartedInfo.TaskKind |
Exception | Description |
---|---|
IfMismatchException |
this exception thrown if an if-sequent match failed
|
MissingInstantiationException | |
MissingSortException | |
SortMismatchException | |
SVInstantiationException | |
SVInstantiationExceptionWithPosition |
Represents an exception with position information.
|
SVInstantiationParserException | |
SVRigidnessException |