de.uka.ilkd.key.proof.init

Class JavaProfile

java.lang.Object

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

de.uka.ilkd.key.proof.init.JavaProfile

All Implemented Interfaces:

Profile

Direct Known Subclasses:

SimplifyTermProfile, SymbolicExecutionJavaProfile

public class JavaProfile
extends AbstractProfile

This profile sets up KeY for verification of JavaCard programs.

Field Summary

Fields

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

Constructor Summary

Constructors

Modifier	Constructor and Description
	JavaProfile()
private	JavaProfile(boolean perms)
protected	JavaProfile(java.lang.String standardRules)

Method Summary

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()

Methods inherited from class de.uka.ilkd.key.proof.init.AbstractProfile

computeSupportedGoalChooserBuilder, getDefaultGoalChooserBuilder, getDefaultProfile, getInternalClassDirectory, getInternalClasslistFilename, getSelectedGoalChooserBuilder, getStandardRules, getStrategyFactory, getTermLabelManager, initTermLabelManager, lookupGC, setDefaultProfile, setSelectedGoalChooserBuilder, supportedGoalChoosers, supportedStrategies, supportsStrategyFactory

Methods inherited from class java.lang.Object

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

Field Detail

NAME

public static final java.lang.String NAME

See Also:

Constant Field Values

NAME_WITH_PERMISSIONS

public static final java.lang.String NAME_WITH_PERMISSIONS

See Also:

Constant Field Values

defaultInstance

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 Threads (not the UI Thread).

defaultInstancePermissions

public static JavaProfile defaultInstancePermissions

DEFAULT

public static final StrategyFactory DEFAULT

permissions

private boolean permissions

oneStepSimpilifier

private OneStepSimplifier oneStepSimpilifier

Constructor Detail

JavaProfile

protected JavaProfile(java.lang.String standardRules)

JavaProfile

public JavaProfile()

JavaProfile

private JavaProfile(boolean perms)

Method Detail

computeTermLabelConfiguration

protected ImmutableList<TermLabelManager.TermLabelConfiguration> computeTermLabelConfiguration()

Computes the TermLabelManager.TermLabelConfiguration to use in this Profile.

Specified by:

computeTermLabelConfiguration in class AbstractProfile

Returns:

The TermLabelManager.TermLabelConfiguration to use in this Profile.

getStrategyFactories

protected ImmutableSet<StrategyFactory> getStrategyFactories()

Overrides:

getStrategyFactories in class AbstractProfile

initBuiltInRules

protected ImmutableList<BuiltInRule> initBuiltInRules()

Overrides:

initBuiltInRules in class AbstractProfile

getOneStepSimpilifier

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.

Returns:

The OneStepSimplifier instance to use.

getJustification

public RuleJustification getJustification(Rule r)

determines the justification of rule r. For a method contract rule it returns a new instance of a ComplexRuleJustification otherwise the rule justification determined by the super class is returned

Specified by:

getJustification in interface Profile

Overrides:

getJustification in class AbstractProfile

Parameters:

r - the rule described above

Returns:

justification for the given rule

name

public java.lang.String name()

the name of the profile

Returns:

the name

getDefaultStrategyFactory

public StrategyFactory getDefaultStrategyFactory()

the default strategy factory to be used

Returns:

the default strategy factory

getDefaultInstance

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 Threads (not the UI Thread).

Parameters:

perms - boolean to decide whether we use permissions

Returns:

The default instance for usage in the Thread of the user interface.

getDefaultInstance

public static JavaProfile getDefaultInstance()

withPermissions

public boolean withPermissions()

isSpecificationInvolvedInRuleApp

public boolean isSpecificationInvolvedInRuleApp(RuleApp app)