de.uka.ilkd.key.proof.init

Interface Profile

All Known Implementing Classes:

AbstractProfile, JavaProfile, SimplifyTermProfile, SymbolicExecutionJavaProfile

public interface Profile

This interface provides methods that allow to customize KeY for certain applications. It supports to customize

• the rule base to be used
• the available strategies
• the goal selection strategy
• the way how term labels are maintained

Currently this is only rudimentary: possible extensions are

• program model to use (java, misrac, csharp)
• integrate in plug-in framework allow addition of menu entries toolbar buttons etc.

etc.

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 Proofs are done in parallel (in different Threads), 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).

Method Summary

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.

Method Detail

getStandardRules

RuleCollection getStandardRules()

returns the rule source containg all taclets for this profile

name

java.lang.String name()

the name of this profile

supportedStrategies

ImmutableSet<StrategyFactory> supportedStrategies()

returns the strategy factories for the supported strategies

getDefaultStrategyFactory

StrategyFactory getDefaultStrategyFactory()

returns the strategy factory for the default strategy of this profile

supportsStrategyFactory

boolean supportsStrategyFactory(Name strategyName)

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

Returns:

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

getStrategyFactory

StrategyFactory getStrategyFactory(Name strategyName)

returns the StrategyFactory for strategy strategyName

Parameters:

strategyName - the Name of the strategy

Returns:

the StrategyFactory to build the demanded strategy

supportedGoalChoosers

ImmutableSet<java.lang.String> supportedGoalChoosers()

returns the names of possible goalchoosers to be used by the automatic prover environment

getDefaultGoalChooserBuilder

GoalChooserBuilder getDefaultGoalChooserBuilder()

returns the default builder for a goal chooser

setSelectedGoalChooserBuilder

void setSelectedGoalChooserBuilder(java.lang.String name)

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

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

getSelectedGoalChooserBuilder

GoalChooserBuilder getSelectedGoalChooserBuilder()

returns a new builder instance for the selected goal choooser

getJustification

RuleJustification getJustification(Rule r)

returns the (default) justification for the given rule

getInternalClassDirectory

java.lang.String getInternalClassDirectory()

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

Returns:

the file name of the internal class directory relative to JavaRedux

getInternalClasslistFilename

java.lang.String getInternalClasslistFilename()

returns the file name of the internal class list

Returns:

the file name of the internal class list

getTermLabelManager

TermLabelManager getTermLabelManager()

isSpecificationInvolvedInRuleApp

boolean isSpecificationInvolvedInRuleApp(RuleApp app)