public class JavaCardDLStrategyFactory extends Object implements StrategyFactory
Constructor and Description |
---|
JavaCardDLStrategyFactory() |
Modifier and Type | Method and Description |
---|---|
Strategy |
create(Proof p_proof,
StrategyProperties strategyProperties)
Create strategy for a proof.
|
StrategySettingsDefinition |
getSettingsDefinition()
Returns the
StrategySettingsDefinition which describes
how an user interface has to look like to edit StrategySettings
supported by created Strategy instances. |
Name |
name()
returns the name of this element
|
static String |
TOOL_TIP_USER_HIGH(int i) |
static String |
TOOL_TIP_USER_LOW(int i) |
static String |
TOOL_TIP_USER_OFF(int i) |
public static final Name NAME
Name
of this StrategyFactory
.public static final String TOOL_TIP_STOP_AT_DEFAULT
public static final String TOOL_TIP_STOP_AT_UNCLOSABLE
public static final String TOOL_TIP_PROOF_SPLITTING_FREE
public static final String TOOL_TIP_PROOF_SPLITTING_DELAYED
public static final String TOOL_TIP_PROOF_SPLITTING_OFF
public static final String TOOL_TIP_LOOP_INVARIANT
public static final String TOOL_TIP_LOOP_EXPAND
public static final String TOOL_TIP_LOOP_NONE
public static final String TOOL_TIP_BLOCK_CONTRACT
public static final String TOOL_TIP_BLOCK_EXPAND
public static final String TOOL_TIP_METHOD_CONTRACT
public static final String TOOL_TIP_METHOD_EXPAND
public static final String TOOL_TIP_METHOD_NONE
public static final String TOOL_TIP_CLASSAXIOM_FREE
public static final String TOOL_TIP_CLASSAXIOM_DELAYED
public static final String TOOL_TIP_CLASSAXIOM_OFF
public static final String TOOL_TIP_DEPENDENCY_ON
public static final String TOOL_TIP_DEPENDENCY_OFF
public static final String TOOL_TIP_QUERY_ON
public static final String TOOL_TIP_QUERY_RESTRICTED
public static final String TOOL_TIP_QUERY_OFF
public static final String TOOL_TIP_EXPAND_LOCAL_QUERIES_ON
public static final String TOOL_TIP_EXPAND_LOCAL_QUERIES_OFF
public static final String TOOL_TIP_ARITHMETIC_BASE
public static final String TOOL_TIP_ARITHMETIC_DEF_OPS
public static final String TOOL_TIP_ARITHMETIC_MODEL_SEARCH
public static final String TOOL_TIP_QUANTIFIER_NONE
public static final String TOOL_TIP_QUANTIFIER_NO_SPLITS
public static final String TOOL_TIP_QUANTIFIER_NO_SPLITS_WITH_PROGS
public static final String TOOL_TIP_QUANTIFIER_FREE
public static final String TOOL_TIP_AUTO_INDUCTION_ON
public static final String TOOL_TIP_AUTO_INDUCTION_RESTRICTED
public static final String TOOL_TIP_AUTO_INDUCTION_OFF
public static String TOOL_TIP_USER_OFF(int i)
public static String TOOL_TIP_USER_LOW(int i)
public static String TOOL_TIP_USER_HIGH(int i)
public Strategy create(Proof p_proof, StrategyProperties strategyProperties)
StrategyFactory
create
in interface StrategyFactory
p_proof
- the Proof a strategy is created forstrategyProperties
- the StrategyProperties to customize the
strategypublic StrategySettingsDefinition getSettingsDefinition()
StrategyFactory
StrategySettingsDefinition
which describes
how an user interface has to look like to edit StrategySettings
supported by created Strategy
instances.getSettingsDefinition
in interface StrategyFactory
StrategySettingsDefinition
which describes the user interface.