de.uka.ilkd.key.proof.init

Class AbstractProfile

java.lang.Object

de.uka.ilkd.key.proof.init.AbstractProfile

All Implemented Interfaces:

Profile

Direct Known Subclasses:

JavaProfile

public abstract class AbstractProfile
extends java.lang.Object
implements Profile

Field Summary

Fields

Modifier and Type	Field and Description
private static Profile	defaultProfile The default profile which is used if no profile is defined in custom problem files (loaded via KeYUserProblemFile).
private GoalChooserBuilder	prototype
private RuleCollection	standardRules
private ImmutableSet<StrategyFactory>	strategies
private ImmutableSet<java.lang.String>	supportedGC
private ImmutableSet<GoalChooserBuilder>	supportedGCB
private TermLabelManager	termLabelManager

Constructor Summary

Constructors

Modifier	Constructor and Description
protected	AbstractProfile(java.lang.String standardRuleFilename)

Method Summary

Modifier and Type	Method and Description
protected ImmutableSet<GoalChooserBuilder>	computeSupportedGoalChooserBuilder()
protected abstract ImmutableList<TermLabelManager.TermLabelConfiguration>	computeTermLabelConfiguration() Computes the TermLabelManager.TermLabelConfiguration to use in this Profile.
private static ImmutableSet<java.lang.String>	extractNames(ImmutableSet<GoalChooserBuilder> supportedGCB)
GoalChooserBuilder	getDefaultGoalChooserBuilder() returns the default builder for a goal chooser
static Profile	getDefaultProfile() Returns the default profile which is used if no profile is defined in custom problem files (loaded via KeYUserProblemFile).
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) any standard rule has is by default justified by an axiom rule justification
GoalChooserBuilder	getSelectedGoalChooserBuilder() returns a copy of the selected goal chooser builder
RuleCollection	getStandardRules() returns the rule source containg all taclets for this profile
protected ImmutableSet<StrategyFactory>	getStrategyFactories()
StrategyFactory	getStrategyFactory(Name n) returns the StrategyFactory for strategy strategyName
TermLabelManager	getTermLabelManager()
protected ImmutableList<BuiltInRule>	initBuiltInRules()
protected void	initTermLabelManager() Initializes the TermLabelManager.
GoalChooserBuilder	lookupGC(java.lang.String name) looks up the demanded goal chooser is supported and returns a new instance if possible otherwise null is returned
static void	setDefaultProfile(Profile defaultProfile) Sets the default profile which is used if no profile is defined in custom problem files (loaded via KeYUserProblemFile).
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 the supported goal chooser builders
ImmutableSet<StrategyFactory>	supportedStrategies() returns the strategy factories for the supported strategies
boolean	supportsStrategyFactory(Name strategy) returns true if strategy strategyName may be used with this profile.

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Methods inherited from interface de.uka.ilkd.key.proof.init.Profile

getDefaultStrategyFactory, isSpecificationInvolvedInRuleApp, name

Field Detail

defaultProfile

private static Profile defaultProfile

The default profile which is used if no profile is defined in custom problem files (loaded via KeYUserProblemFile).

standardRules

private final RuleCollection standardRules

strategies

private final ImmutableSet<StrategyFactory> strategies

supportedGC

private final ImmutableSet<java.lang.String> supportedGC

supportedGCB

private final ImmutableSet<GoalChooserBuilder> supportedGCB

prototype

private GoalChooserBuilder prototype

termLabelManager

private TermLabelManager termLabelManager

Constructor Detail

AbstractProfile

protected AbstractProfile(java.lang.String standardRuleFilename)

Method Detail

extractNames

private static ImmutableSet<java.lang.String> extractNames(ImmutableSet<GoalChooserBuilder> supportedGCB)

computeSupportedGoalChooserBuilder

protected ImmutableSet<GoalChooserBuilder> computeSupportedGoalChooserBuilder()

initTermLabelManager

protected void initTermLabelManager()

Initializes the TermLabelManager.

computeTermLabelConfiguration

protected abstract ImmutableList<TermLabelManager.TermLabelConfiguration> computeTermLabelConfiguration()

Computes the TermLabelManager.TermLabelConfiguration to use in this Profile.

Returns:

The TermLabelManager.TermLabelConfiguration to use in this Profile.

getStandardRules

public RuleCollection getStandardRules()

Description copied from interface: Profile

returns the rule source containg all taclets for this profile

Specified by:

getStandardRules in interface Profile

getStrategyFactories

protected ImmutableSet<StrategyFactory> getStrategyFactories()

initBuiltInRules

protected ImmutableList<BuiltInRule> initBuiltInRules()

supportedStrategies

public ImmutableSet<StrategyFactory> supportedStrategies()

Description copied from interface: Profile

returns the strategy factories for the supported strategies

Specified by:

supportedStrategies in interface Profile

supportsStrategyFactory

public boolean supportsStrategyFactory(Name strategy)

Description copied from interface: Profile

returns true if strategy strategyName may be used with this profile.

Specified by:

supportsStrategyFactory in interface Profile

Returns:

supportedStrategies()->exists(s | s.name.equals(strategyName))

getStrategyFactory

public StrategyFactory getStrategyFactory(Name n)

Description copied from interface: Profile

returns the StrategyFactory for strategy strategyName

Specified by:

getStrategyFactory in interface Profile

Parameters:

n - the Name of the strategy

Returns:

the StrategyFactory to build the demanded strategy

supportedGoalChoosers

public ImmutableSet<java.lang.String> supportedGoalChoosers()

returns the names of the supported goal chooser builders

Specified by:

supportedGoalChoosers in interface Profile

getDefaultGoalChooserBuilder

public GoalChooserBuilder getDefaultGoalChooserBuilder()

returns the default builder for a goal chooser

Specified by:

getDefaultGoalChooserBuilder in interface Profile

Returns:

this implementation returns a new instance of DefaultGoalChooserBuilder

setSelectedGoalChooserBuilder

public void setSelectedGoalChooserBuilder(java.lang.String name)

sets the user selected goal chooser builder to be used as prototype

Specified by:

setSelectedGoalChooserBuilder in interface Profile

Parameters:

name - the String with the name of the goal chooser to be used

Throws:

java.lang.IllegalArgumentException - if a goal chooser of the given name is not supported

lookupGC

public GoalChooserBuilder lookupGC(java.lang.String name)

looks up the demanded goal chooser is supported and returns a new instance if possible otherwise null is returned

Parameters:

name - the String with the goal choosers name

Returns:

a new instance of the builder or null if the demanded chooser is not supported

getSelectedGoalChooserBuilder

public GoalChooserBuilder getSelectedGoalChooserBuilder()

returns a copy of the selected goal chooser builder

Specified by:

getSelectedGoalChooserBuilder in interface Profile

getJustification

public RuleJustification getJustification(Rule r)

any standard rule has is by default justified by an axiom rule justification

Specified by:

getJustification in interface Profile

Returns:

the justification for the standard rules

getInternalClassDirectory

public java.lang.String getInternalClassDirectory()

Description copied from interface: Profile

returns the file name of the internal class directory relative to JavaRedux

Specified by:

getInternalClassDirectory in interface Profile

Returns:

the file name of the internal class directory relative to JavaRedux

getInternalClasslistFilename

public java.lang.String getInternalClasslistFilename()

Description copied from interface: Profile

returns the file name of the internal class list

Specified by:

getInternalClasslistFilename in interface Profile

Returns:

the file name of the internal class list

getDefaultProfile

public static Profile getDefaultProfile()

Returns the default profile which is used if no profile is defined in custom problem files (loaded via KeYUserProblemFile).

Returns:

The default profile which is used if no profile is defined in custom problem files (loaded via KeYUserProblemFile).

setDefaultProfile

public static void setDefaultProfile(Profile defaultProfile)

Sets the default profile which is used if no profile is defined in custom problem files (loaded via KeYUserProblemFile).

Parameters:

defaultProfile - The default profile which is used if no profile is defined in custom problem files (loaded via KeYUserProblemFile).

getTermLabelManager

public TermLabelManager getTermLabelManager()

Specified by:

getTermLabelManager in interface Profile