| Class | Description |
|---|---|
| AbstractProverCore |
Common class for provers which takes care of listener registration and task event propagation
|
| AppliedRuleStopCondition |
Implementation of
StopCondition which stops the strategy
after a reached limit of rules or after a timeout in ms. |
| ApplyStrategy |
Applies rules in an automated fashion.
|
| ApplyStrategyInfo |
The final result of the strategy application is stored in this container
and returned to the instance that started the strategies.
|
| 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 | |
| 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.
|