public class JavaProfile extends AbstractProfile
Modifier and Type | Field and Description |
---|---|
static StrategyFactory |
DEFAULT |
static JavaProfile |
defaultInstance
The default instance of this class.
|
static JavaProfile |
defaultInstancePermissions |
static java.lang.String |
NAME |
static java.lang.String |
NAME_WITH_PERMISSIONS |
private OneStepSimplifier |
oneStepSimpilifier |
private boolean |
permissions |
Modifier | Constructor and Description |
---|---|
|
JavaProfile() |
private |
JavaProfile(boolean perms) |
protected |
JavaProfile(java.lang.String standardRules) |
Modifier and Type | Method and Description |
---|---|
protected ImmutableList<TermLabelManager.TermLabelConfiguration> |
computeTermLabelConfiguration()
Computes the
TermLabelManager.TermLabelConfiguration to use in this Profile . |
static JavaProfile |
getDefaultInstance() |
static JavaProfile |
getDefaultInstance(boolean perms)
Returns the default instance of this class.
|
StrategyFactory |
getDefaultStrategyFactory()
the default strategy factory to be used
|
RuleJustification |
getJustification(Rule r)
determines the justification of rule
r . |
OneStepSimplifier |
getOneStepSimpilifier()
Returns the
OneStepSimplifier instance which should be used
in this JavaProfile . |
protected ImmutableSet<StrategyFactory> |
getStrategyFactories() |
protected ImmutableList<BuiltInRule> |
initBuiltInRules() |
boolean |
isSpecificationInvolvedInRuleApp(RuleApp app) |
java.lang.String |
name()
the name of the profile
|
boolean |
withPermissions() |
computeSupportedGoalChooserBuilder, getDefaultGoalChooserBuilder, getDefaultProfile, getInternalClassDirectory, getInternalClasslistFilename, getSelectedGoalChooserBuilder, getStandardRules, getStrategyFactory, getTermLabelManager, initTermLabelManager, lookupGC, setDefaultProfile, setSelectedGoalChooserBuilder, supportedGoalChoosers, supportedStrategies, supportsStrategyFactory
public static final java.lang.String NAME
public static final java.lang.String NAME_WITH_PERMISSIONS
public static JavaProfile defaultInstance
The default instance of this class.
It is typically used in the Thread
of the user interface.
Other instances of this class are typically only required to
use them in different Thread
s (not the UI Thread
).
public static JavaProfile defaultInstancePermissions
public static final StrategyFactory DEFAULT
private boolean permissions
private OneStepSimplifier oneStepSimpilifier
protected JavaProfile(java.lang.String standardRules)
public JavaProfile()
private JavaProfile(boolean perms)
protected ImmutableList<TermLabelManager.TermLabelConfiguration> computeTermLabelConfiguration()
TermLabelManager.TermLabelConfiguration
to use in this Profile
.computeTermLabelConfiguration
in class AbstractProfile
TermLabelManager.TermLabelConfiguration
to use in this Profile
.protected ImmutableSet<StrategyFactory> getStrategyFactories()
getStrategyFactories
in class AbstractProfile
protected ImmutableList<BuiltInRule> initBuiltInRules()
initBuiltInRules
in class AbstractProfile
public OneStepSimplifier getOneStepSimpilifier()
Returns the OneStepSimplifier
instance which should be used
in this JavaProfile
. It is added to the build in rules via
initBuiltInRules()
.
Sub profiles may exchange the OneStepSimplifier
instance,
for instance for site proofs used in the symbolic execution tree extraction.
OneStepSimplifier
instance to use.public RuleJustification getJustification(Rule r)
r
. For a method contract rule it
returns a new instance of a ComplexRuleJustification
otherwise the rule
justification determined by the super class is returnedgetJustification
in interface Profile
getJustification
in class AbstractProfile
r
- the rule described abovepublic java.lang.String name()
public StrategyFactory getDefaultStrategyFactory()
public static JavaProfile getDefaultInstance(boolean perms)
Returns the default instance of this class.
It is typically used in the Thread
of the user interface.
Other instances of this class are typically only required to
use them in different Thread
s (not the UI Thread
).
perms
- boolean to decide whether we use permissionsThread
of the user interface.public static JavaProfile getDefaultInstance()
public boolean withPermissions()
public boolean isSpecificationInvolvedInRuleApp(RuleApp app)