public interface Profile
This interface provides methods that allow to customize KeY for certain applications. It supports to customize
Each Profile
has a unique name name()
.
It is recommended
to have only one instance of each Profile
. The default instances
for usage in the Thread
of the user interface
are available via JavaProfile.getDefaultInstance()
and
SymbolicExecutionJavaProfile#getDefaultInstance()
.
It is possible to get the default instance for a given name via
AbstractProfile#getDefaultInstanceForName(String)
. Multiple instances
are only required if Proof
s are done in parallel (in different Thread
s),
because some rules might have a state (at the moment this is only the OneStepSimplifier
).
The default Profile
which is used if no profile is programatically
(or via a custom problem file) defined is AbstractProfile.getDefaultProfile()
.
It can be changed via AbstractProfile.setDefaultProfile(Profile)
.
Modifier and Type | Method and Description |
---|---|
GoalChooserBuilder |
getDefaultGoalChooserBuilder()
returns the default builder for a goal chooser
|
StrategyFactory |
getDefaultStrategyFactory()
returns the strategy factory for the default strategy of this profile
|
java.lang.String |
getInternalClassDirectory()
returns the file name of the internal class directory relative to JavaRedux
|
java.lang.String |
getInternalClasslistFilename()
returns the file name of the internal class list
|
RuleJustification |
getJustification(Rule r)
returns the (default) justification for the given rule
|
GoalChooserBuilder |
getSelectedGoalChooserBuilder()
returns a new builder instance for the selected goal choooser
|
RuleCollection |
getStandardRules()
returns the rule source containg all taclets for this profile
|
StrategyFactory |
getStrategyFactory(Name strategyName)
returns the StrategyFactory for strategy
strategyName |
TermLabelManager |
getTermLabelManager() |
boolean |
isSpecificationInvolvedInRuleApp(RuleApp app) |
java.lang.String |
name()
the name of this profile
|
void |
setSelectedGoalChooserBuilder(java.lang.String name)
sets the user selected goal chooser builder to be used as prototype
|
ImmutableSet<java.lang.String> |
supportedGoalChoosers()
returns the names of possible goalchoosers to be used by the
automatic prover environment
|
ImmutableSet<StrategyFactory> |
supportedStrategies()
returns the strategy factories for the supported strategies
|
boolean |
supportsStrategyFactory(Name strategyName)
returns true if strategy
strategyName may be
used with this profile. |
RuleCollection getStandardRules()
java.lang.String name()
ImmutableSet<StrategyFactory> supportedStrategies()
StrategyFactory getDefaultStrategyFactory()
boolean supportsStrategyFactory(Name strategyName)
strategyName
may be
used with this profile.StrategyFactory getStrategyFactory(Name strategyName)
strategyName
strategyName
- the Name of the strategyImmutableSet<java.lang.String> supportedGoalChoosers()
GoalChooserBuilder getDefaultGoalChooserBuilder()
void setSelectedGoalChooserBuilder(java.lang.String name)
name
- the String with the name of the goal chooser to be usedjava.lang.IllegalArgumentException
- if a goal chooser of the given name is not
supportedGoalChooserBuilder getSelectedGoalChooserBuilder()
RuleJustification getJustification(Rule r)
java.lang.String getInternalClassDirectory()
java.lang.String getInternalClasslistFilename()
TermLabelManager getTermLabelManager()
boolean isSpecificationInvolvedInRuleApp(RuleApp app)