public class JavaCardDLStrategyFactory extends java.lang.Object implements StrategyFactory
Modifier and Type | Field and Description |
---|---|
static Name |
NAME
The unique
Name of this StrategyFactory . |
static java.lang.String |
TOOL_TIP_ARITHMETIC_BASE |
static java.lang.String |
TOOL_TIP_ARITHMETIC_DEF_OPS |
static java.lang.String |
TOOL_TIP_ARITHMETIC_MODEL_SEARCH |
static java.lang.String |
TOOL_TIP_AUTO_INDUCTION_OFF |
static java.lang.String |
TOOL_TIP_AUTO_INDUCTION_ON |
static java.lang.String |
TOOL_TIP_AUTO_INDUCTION_RESTRICTED |
static java.lang.String |
TOOL_TIP_BLOCK_CONTRACT_EXTERNAL |
static java.lang.String |
TOOL_TIP_BLOCK_CONTRACT_INTERNAL |
static java.lang.String |
TOOL_TIP_BLOCK_EXPAND |
static java.lang.String |
TOOL_TIP_CLASSAXIOM_DELAYED |
static java.lang.String |
TOOL_TIP_CLASSAXIOM_FREE |
static java.lang.String |
TOOL_TIP_CLASSAXIOM_OFF |
static java.lang.String |
TOOL_TIP_DEPENDENCY_OFF |
static java.lang.String |
TOOL_TIP_DEPENDENCY_ON |
static java.lang.String |
TOOL_TIP_EXPAND_LOCAL_QUERIES_OFF |
static java.lang.String |
TOOL_TIP_EXPAND_LOCAL_QUERIES_ON |
static java.lang.String |
TOOL_TIP_LOOP_EXPAND |
static java.lang.String |
TOOL_TIP_LOOP_INVARIANT |
static java.lang.String |
TOOL_TIP_LOOP_NONE |
static java.lang.String |
TOOL_TIP_LOOP_SCOPE_INVARIANT |
static java.lang.String |
TOOL_TIP_METHOD_CONTRACT |
static java.lang.String |
TOOL_TIP_METHOD_EXPAND |
static java.lang.String |
TOOL_TIP_METHOD_NONE |
static java.lang.String |
TOOL_TIP_MPS_MERGE |
static java.lang.String |
TOOL_TIP_MPS_NONE |
static java.lang.String |
TOOL_TIP_MPS_SKIP |
static java.lang.String |
TOOL_TIP_OSS_OFF |
static java.lang.String |
TOOL_TIP_OSS_ON |
static java.lang.String |
TOOL_TIP_PROOF_SPLITTING_DELAYED |
static java.lang.String |
TOOL_TIP_PROOF_SPLITTING_FREE |
static java.lang.String |
TOOL_TIP_PROOF_SPLITTING_OFF |
static java.lang.String |
TOOL_TIP_QUANTIFIER_FREE |
static java.lang.String |
TOOL_TIP_QUANTIFIER_NO_SPLITS |
static java.lang.String |
TOOL_TIP_QUANTIFIER_NO_SPLITS_WITH_PROGS |
static java.lang.String |
TOOL_TIP_QUANTIFIER_NONE |
static java.lang.String |
TOOL_TIP_QUERY_OFF |
static java.lang.String |
TOOL_TIP_QUERY_ON |
static java.lang.String |
TOOL_TIP_QUERY_RESTRICTED |
static java.lang.String |
TOOL_TIP_STOP_AT_DEFAULT |
static java.lang.String |
TOOL_TIP_STOP_AT_UNCLOSABLE |
Constructor and Description |
---|
JavaCardDLStrategyFactory() |
public static final Name NAME
Name
of this StrategyFactory
.public static final java.lang.String TOOL_TIP_STOP_AT_DEFAULT
public static final java.lang.String TOOL_TIP_STOP_AT_UNCLOSABLE
public static final java.lang.String TOOL_TIP_OSS_ON
public static final java.lang.String TOOL_TIP_OSS_OFF
public static final java.lang.String TOOL_TIP_PROOF_SPLITTING_FREE
public static final java.lang.String TOOL_TIP_PROOF_SPLITTING_DELAYED
public static final java.lang.String TOOL_TIP_PROOF_SPLITTING_OFF
public static final java.lang.String TOOL_TIP_LOOP_INVARIANT
public static final java.lang.String TOOL_TIP_LOOP_SCOPE_INVARIANT
public static final java.lang.String TOOL_TIP_LOOP_EXPAND
public static final java.lang.String TOOL_TIP_LOOP_NONE
public static final java.lang.String TOOL_TIP_BLOCK_CONTRACT_INTERNAL
public static final java.lang.String TOOL_TIP_BLOCK_CONTRACT_EXTERNAL
public static final java.lang.String TOOL_TIP_BLOCK_EXPAND
public static final java.lang.String TOOL_TIP_METHOD_CONTRACT
public static final java.lang.String TOOL_TIP_METHOD_EXPAND
public static final java.lang.String TOOL_TIP_METHOD_NONE
public static final java.lang.String TOOL_TIP_MPS_MERGE
public static final java.lang.String TOOL_TIP_MPS_SKIP
public static final java.lang.String TOOL_TIP_MPS_NONE
public static final java.lang.String TOOL_TIP_CLASSAXIOM_FREE
public static final java.lang.String TOOL_TIP_CLASSAXIOM_DELAYED
public static final java.lang.String TOOL_TIP_CLASSAXIOM_OFF
public static final java.lang.String TOOL_TIP_DEPENDENCY_ON
public static final java.lang.String TOOL_TIP_DEPENDENCY_OFF
public static final java.lang.String TOOL_TIP_QUERY_ON
public static final java.lang.String TOOL_TIP_QUERY_RESTRICTED
public static final java.lang.String TOOL_TIP_QUERY_OFF
public static final java.lang.String TOOL_TIP_EXPAND_LOCAL_QUERIES_ON
public static final java.lang.String TOOL_TIP_EXPAND_LOCAL_QUERIES_OFF
public static final java.lang.String TOOL_TIP_ARITHMETIC_BASE
public static final java.lang.String TOOL_TIP_ARITHMETIC_DEF_OPS
public static final java.lang.String TOOL_TIP_ARITHMETIC_MODEL_SEARCH
public static final java.lang.String TOOL_TIP_QUANTIFIER_NONE
public static final java.lang.String TOOL_TIP_QUANTIFIER_NO_SPLITS
public static final java.lang.String TOOL_TIP_QUANTIFIER_NO_SPLITS_WITH_PROGS
public static final java.lang.String TOOL_TIP_QUANTIFIER_FREE
public static final java.lang.String TOOL_TIP_AUTO_INDUCTION_ON
public static final java.lang.String TOOL_TIP_AUTO_INDUCTION_RESTRICTED
public static final java.lang.String TOOL_TIP_AUTO_INDUCTION_OFF
public static final java.lang.String toolTipUserOff(int i)
public static final java.lang.String toolTipUserLow(int i)
public static final java.lang.String toolTipUserHigh(int i)
private static OneOfStrategyPropertyDefinition getStopAt()
private static OneOfStrategyPropertyDefinition getOssUsage()
private static OneOfStrategyPropertyDefinition getProofSplitting()
private static OneOfStrategyPropertyDefinition getLoopTreatment()
private static OneOfStrategyPropertyDefinition getBlockTreatment()
private static OneOfStrategyPropertyDefinition getMethodTreatment()
private static OneOfStrategyPropertyDefinition getMergePointStatementTreatment()
private static OneOfStrategyPropertyDefinition getDependencyContracts()
private static OneOfStrategyPropertyDefinition getQueryTreatment()
private static OneOfStrategyPropertyDefinition getArithmeticTreatment()
private static OneOfStrategyPropertyDefinition getQuantifierTreatment()
private static OneOfStrategyPropertyDefinition getClassAxiom()
private static OneOfStrategyPropertyDefinition getAutoInduction()
private static OneOfStrategyPropertyDefinition getUserOptions()
public Strategy create(Proof proof, StrategyProperties strategyProperties)
StrategyFactory
create
in interface StrategyFactory
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.