Package | Description |
---|---|
de.uka.ilkd.key.prover.impl | |
de.uka.ilkd.key.settings | |
de.uka.ilkd.key.strategy |
This package contains classes implementing the proof search strategies of KeY.
|
de.uka.ilkd.key.symbolic_execution.strategy |
Modifier and Type | Class and Description |
---|---|
class |
AppliedRuleStopCondition
Implementation of
StopCondition which stops the strategy
after a reached limit of rules or after a timeout in ms. |
Modifier and Type | Method and Description |
---|---|
StopCondition |
StrategySettings.getApplyStrategyStopCondition()
Returns the
StopCondition to use in an ApplyStrategy
instance to determine after each applied rule if more rules
should be applied or not. |
StopCondition |
StrategySettings.getCustomApplyStrategyStopCondition()
Returns a customized
StopCondition which is used in an
ApplyStrategy to determine after each applied rule if more rules
should be applied or not. |
Modifier and Type | Method and Description |
---|---|
void |
StrategySettings.setCustomApplyStrategyStopCondition(StopCondition customApplyStrategyStopCondition)
Defines the
StopCondition which is used in an
ApplyStrategy to determine after each applied rule if more rules
should be applied or not. |
Modifier and Type | Interface and Description |
---|---|
interface |
IBreakpointStopCondition
Defines the basic functionality of an
StopCondition which
stops applying rules when at least one IBreakpoint is hit. |
Modifier and Type | Class and Description |
---|---|
class |
AbstractCallStackBasedStopCondition
Provides the basic functionality for
StopCondition s which stops
the auto mode when the call stack size of the starting set node has
a special difference to the call stack size of the current set node, e.g. |
class |
BreakpointStopCondition
An
IBreakpointStopCondition which can be used during proof. |
class |
CompoundStopCondition
This
StopCondition contains other StopCondition as
children and stops the auto mode if at least on of its children force it. |
class |
ExecutedSymbolicExecutionTreeNodesStopCondition
This
StopCondition stops the auto mode (ApplyStrategy ) if
a given number (ExecutedSymbolicExecutionTreeNodesStopCondition.getMaximalNumberOfSetNodesToExecutePerGoal() ) of maximal
executed symbolic execution tree nodes is reached in a goal. |
class |
StepOverSymbolicExecutionTreeNodesStopCondition
This
StopCondition stops the auto mode when a "step over" is completed. |
class |
StepReturnSymbolicExecutionTreeNodesStopCondition
This
StopCondition stops the auto mode when a "step over" is completed. |
class |
SymbolicExecutionBreakpointStopCondition
An
IBreakpointStopCondition which can be used during symbolic execution. |
Modifier and Type | Method and Description |
---|---|
java.util.List<StopCondition> |
CompoundStopCondition.getChildren() |
Modifier and Type | Method and Description |
---|---|
void |
CompoundStopCondition.addChildren(StopCondition... children)
Adds new child
StopCondition s. |
void |
CompoundStopCondition.removeChild(StopCondition child) |
Constructor and Description |
---|
CompoundStopCondition(StopCondition... children)
Constructor.
|
Copyright © 2003-2019 The KeY-Project.