Package | Description |
---|---|
de.uka.ilkd.key.gui |
This package contains classes forming the graphical user interface of KeY.
|
de.uka.ilkd.key.informationflow.macros | |
de.uka.ilkd.key.macros | |
de.uka.ilkd.key.proof |
This package contains the core data structures of proofs, nodes, goals, as well
as machinery to deal with these data structures.
|
de.uka.ilkd.key.strategy |
This package contains classes implementing the proof search strategies of KeY.
|
de.uka.ilkd.key.symbolic_execution.strategy | |
de.uka.ilkd.key.util |
This package is a grab bag of miscellaneous useful code fragments.
|
Modifier and Type | Method and Description |
---|---|
Strategy |
StrategySelectionView.getStrategy(java.lang.String strategyName,
Proof proof,
StrategyProperties properties) |
Modifier and Type | Class and Description |
---|---|
protected class |
UseInformationFlowContractMacro.PropExpansionStrategy
This strategy accepts all rule apps for which the rule name starts with a
string in the admitted set and rejects everything else.
|
Modifier and Type | Method and Description |
---|---|
protected Strategy |
SelfcompositionStateExpansionMacro.createStrategy(Proof proof,
PosInOccurrence posInOcc) |
Modifier and Type | Class and Description |
---|---|
class |
FilterStrategy |
protected class |
PrepareInfFlowContractPreBranchesMacro.RemovePostStrategy
This strategy accepts all rule apps for which the rule name starts with a
string in the admitted set and rejects everything else.
|
Modifier and Type | Method and Description |
---|---|
protected Strategy |
FinishSymbolicExecutionMacro.createStrategy(Proof proof,
PosInOccurrence posInOcc) |
protected Strategy |
AbstractPropositionalExpansionMacro.createStrategy(Proof proof,
PosInOccurrence posInOcc) |
protected Strategy |
PrepareInfFlowContractPreBranchesMacro.createStrategy(Proof proof,
PosInOccurrence posInOcc) |
protected Strategy |
FinishSymbolicExecutionUntilMergePointMacro.createStrategy(Proof proof,
PosInOccurrence posInOcc) |
protected Strategy |
WellDefinednessMacro.createStrategy(Proof proof,
PosInOccurrence posInOcc) |
protected Strategy |
AutoPilotPrepareProofMacro.createStrategy(Proof proof,
PosInOccurrence posInOcc) |
protected abstract Strategy |
StrategyProofMacro.createStrategy(Proof proof,
PosInOccurrence posInOcc) |
protected Strategy |
AutoMacro.createStrategy(Proof proof,
PosInOccurrence posInOcc) |
protected Strategy |
OneStepProofMacro.createStrategy(Proof proof,
PosInOccurrence posInOcc) |
protected Strategy |
AbstractBlastingMacro.createStrategy(Proof proof,
PosInOccurrence posInOcc) |
protected Strategy |
TestGenMacro.createStrategy(Proof proof,
PosInOccurrence posInOcc) |
Constructor and Description |
---|
FilterStrategy(Strategy delegate) |
Modifier and Type | Method and Description |
---|---|
Strategy |
Proof.getActiveStrategy() |
Strategy |
Goal.getGoalStrategy() |
Modifier and Type | Method and Description |
---|---|
void |
Proof.setActiveStrategy(Strategy activeStrategy) |
void |
Goal.setGoalStrategy(Strategy p_goalStrategy) |
Modifier and Type | Class and Description |
---|---|
class |
AbstractFeatureStrategy |
class |
FIFOStrategy
Trivial implementation of the Strategy interface
that uses only the goal time to determine the cost
of a RuleApp.
|
class |
JavaCardDLStrategy
Strategy tailored to be used as long as a java program can be found in the
sequent.
|
class |
SimpleFilteredStrategy
Trivial implementation of the Strategy interface
that uses only the goal time to determine the cost
of a RuleApp.
|
Modifier and Type | Field and Description |
---|---|
static Strategy |
FIFOStrategy.INSTANCE |
Modifier and Type | Method and Description |
---|---|
Strategy |
StrategyFactory.create(Proof proof,
StrategyProperties strategyProperties)
Create strategy for a proof.
|
Strategy |
FIFOStrategy.Factory.create(Proof proof,
StrategyProperties properties) |
Strategy |
JavaCardDLStrategyFactory.create(Proof proof,
StrategyProperties strategyProperties) |
Modifier and Type | Class and Description |
---|---|
class |
SimplifyTermStrategy
|
class |
SymbolicExecutionStrategy
Strategy to use for symbolic execution. |
Modifier and Type | Method and Description |
---|---|
Strategy |
SymbolicExecutionStrategy.Factory.create(Proof proof,
StrategyProperties sp)
Create strategy for a proof.
|
Strategy |
SimplifyTermStrategy.Factory.create(Proof proof,
StrategyProperties sp)
Create strategy for a proof.
|
Modifier and Type | Method and Description |
---|---|
void |
ProofStarter.setStrategy(Strategy strategy) |
Copyright © 2003-2019 The KeY-Project.