de.uka.ilkd.key.rule.label

Class FormulaTermLabelRefactoring

java.lang.Object

de.uka.ilkd.key.rule.label.FormulaTermLabelRefactoring

All Implemented Interfaces:

RuleSpecificTask, TermLabelRefactoring

public class FormulaTermLabelRefactoring
extends java.lang.Object
implements TermLabelRefactoring

The TermLabelRefactoring used to label predicates with a FormulaTermLabel on applied loop invariants or operation contracts.

Author:

Martin Hentschel

Nested Class Summary

Nested classes/interfaces inherited from interface de.uka.ilkd.key.rule.label.TermLabelRefactoring

TermLabelRefactoring.RefactoringScope

Field Summary

Fields

Modifier and Type	Field and Description
private static java.lang.String	INNER_MOST_PARENT_REFACTORED_PREFIX Key prefix used in TermLabelState to store that the inner most label was already refactored on a given Goal.
private static java.lang.String	PARENT_REFACTORING_REQUIRED Key used in TermLabelState by the FormulaTermLabelUpdate to indicate that a refactoring of parents (RefactoringScope#APPLICATION_CHILDREN_AND_GRANDCHILDREN_SUBTREE_AND_PARENTS) is required performed by refactorInCaseOfNewIdRequired(TermLabelState, Goal, Term, Services, List).
private static java.lang.String	SEQUENT_FORMULA_REFACTORING_REQUIRED Key used in TermLabelState by the FormulaTermLabelUpdate to indicate that a refactoring of specified SequentFormulas (RefactoringScope#SEQUENT) is required performed by refactorSequentFormulas(TermLabelState, Services, Term, List).
private static java.lang.String	UPDATE_REFACTORING_REQUIRED Key used in TermLabelState by the StayOnOperatorTermLabelPolicy to indicate that a refactoring below an update (RefactoringScope#APPLICATION_BELOW_UPDATES) is required performed by refactorBewlowUpdates(PosInOccurrence, Term, List).

Constructor Summary

Constructors

Constructor and Description
FormulaTermLabelRefactoring()

Method Summary

Modifier and Type	Method and Description
static void	addSequentFormulaToRefactor(TermLabelState state, SequentFormula sf) Adds the given SequentFormula for refactoring purpose.
static boolean	containsSequentFormulasToRefactor(TermLabelState state) Checks if SequentFormulas to refactor are specified.
TermLabelRefactoring.RefactoringScope	defineRefactoringScope(TermLabelState state, Services services, PosInOccurrence applicationPosInOccurrence, Term applicationTerm, Rule rule, Goal goal, java.lang.Object hint, Term tacletTerm) Defines if a refactoring is required and if so in which TermLabelRefactoring.RefactoringScope.
static java.util.Set<SequentFormula>	getSequentFormulasToRefactor(TermLabelState state) Returns the SequentFormulas to refactor.
ImmutableList<Name>	getSupportedRuleNames() Returns the supported rule Names or null or an empty list if all rules are supported.
static boolean	isInnerMostParentRefactored(TermLabelState state, Goal goal) Checks if the inner most parent was already refactored on the given Goal.
static boolean	isParentRefactroingRequired(TermLabelState state) Checks if a refactoring of parents is required.
static boolean	isUpdateRefactroingRequired(TermLabelState state) Checks if a refactoring below the updates is required.
protected void	refactorBewlowUpdates(PosInOccurrence applicationPosInOccurrence, Term term, java.util.List<TermLabel> labels) Refactors the Term below its update.
void	refactoreLabels(TermLabelState state, Services services, PosInOccurrence applicationPosInOccurrence, Term applicationTerm, Rule rule, Goal goal, java.lang.Object hint, Term tacletTerm, Term term, java.util.List<TermLabel> labels) This method is used to refactor the labels of the given Term.
protected void	refactorInCaseOfNewIdRequired(TermLabelState state, Goal goal, Term term, Services services, java.util.List<TermLabel> labels) Refactors in case that the inner most label needs a new ID.
protected void	refactorSequentFormulas(TermLabelState state, Services services, Term term, java.util.List<TermLabel> labels) Refactors the specified SequentFormulas.
protected void	refactorSpecificationApplication(Term term, Goal goal, Services services, java.util.List<TermLabel> labels, java.lang.Object hint) Refactors a specification application.
protected void	refactorSubstitution(Term term, Term tacletTerm, java.util.List<TermLabel> labels) Refactors the given Term after a substitiution.
static void	setInnerMostParentRefactored(TermLabelState state, Goal goal, boolean refactored) Defines if the inner most parent was already refactored on the given Goal.
static void	setParentRefactroingRequired(TermLabelState state, boolean required) Defines if a refactoring of parents is required.
static void	setUpdateRefactroingRequired(TermLabelState state, boolean required) Defines if a refactoring below the updates is required.
protected boolean	shouldRefactorSpecificationApplication(Rule rule, Goal goal, java.lang.Object hint) Checks if the given hint requires a refactoring.

Methods inherited from class java.lang.Object

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

Field Detail

INNER_MOST_PARENT_REFACTORED_PREFIX

private static final java.lang.String INNER_MOST_PARENT_REFACTORED_PREFIX

Key prefix used in TermLabelState to store that the inner most label was already refactored on a given Goal.

See Also:

Constant Field Values

UPDATE_REFACTORING_REQUIRED

private static final java.lang.String UPDATE_REFACTORING_REQUIRED

Key used in TermLabelState by the StayOnOperatorTermLabelPolicy to indicate that a refactoring below an update (RefactoringScope#APPLICATION_BELOW_UPDATES) is required performed by refactorBewlowUpdates(PosInOccurrence, Term, List).

This is for instance required for the following rules:

• concrete_and_1
• concrete_and_2
• concrete_and_3
• concrete_and_4
• concrete_eq_1
• concrete_eq_2
• concrete_eq_3
• concrete_eq_4
• concrete_impl_1
• concrete_impl_2
• concrete_impl_3
• concrete_impl_4
• concrete_not_1
• concrete_not_2
• concrete_or_1
• concrete_or_2
• concrete_or_3
• concrete_or_4

See Also:

Constant Field Values

PARENT_REFACTORING_REQUIRED

private static final java.lang.String PARENT_REFACTORING_REQUIRED

Key used in TermLabelState by the FormulaTermLabelUpdate to indicate that a refactoring of parents (RefactoringScope#APPLICATION_CHILDREN_AND_GRANDCHILDREN_SUBTREE_AND_PARENTS) is required performed by refactorInCaseOfNewIdRequired(TermLabelState, Goal, Term, Services, List).

This is for instance required if a rule is applied on a sub term without a FormulaTermLabel of a parent which has a FormulaTermLabel. Example rules are:

• ifthenelse_split
• arrayLengthNotNegative

See Also:

Constant Field Values

SEQUENT_FORMULA_REFACTORING_REQUIRED

private static final java.lang.String SEQUENT_FORMULA_REFACTORING_REQUIRED

Key used in TermLabelState by the FormulaTermLabelUpdate to indicate that a refactoring of specified SequentFormulas (RefactoringScope#SEQUENT) is required performed by refactorSequentFormulas(TermLabelState, Services, Term, List).

This is for instance required if the assumes clause of a rule has a FormulaTermLabel but the application does not have it. Example rules are:

• inEqSimp_contradInEq1

See Also:

Constant Field Values

Constructor Detail

FormulaTermLabelRefactoring

public FormulaTermLabelRefactoring()

Method Detail

getSupportedRuleNames

public ImmutableList<Name> getSupportedRuleNames()

Returns the supported rule Names or null or an empty list if all rules are supported.

Specified by:

getSupportedRuleNames in interface RuleSpecificTask

Returns:

The list of supported rule Names or null/empty list if all rules are supported.

defineRefactoringScope

public TermLabelRefactoring.RefactoringScope defineRefactoringScope(TermLabelState state,
                                                                    Services services,
                                                                    PosInOccurrence applicationPosInOccurrence,
                                                                    Term applicationTerm,
                                                                    Rule rule,
                                                                    Goal goal,
                                                                    java.lang.Object hint,
                                                                    Term tacletTerm)

Defines if a refactoring is required and if so in which TermLabelRefactoring.RefactoringScope.

Specified by:

defineRefactoringScope in interface TermLabelRefactoring

Parameters:

state - The TermLabelState of the current rule application.

services - The Services used by the Proof on which a Rule is applied right now.

applicationPosInOccurrence - The PosInOccurrence in the previous Sequent which defines the Term that is rewritten.

applicationTerm - The Term defined by the PosInOccurrence in the previous Sequent.

rule - The Rule which is applied.

goal - The optional Goal on which the Term to create will be used.

hint - An optional hint passed from the active rule to describe the term which should be created.

tacletTerm - The optional taclet Term.

Returns:

The required TermLabelRefactoring.RefactoringScope.

shouldRefactorSpecificationApplication

protected boolean shouldRefactorSpecificationApplication(Rule rule,
                                                         Goal goal,
                                                         java.lang.Object hint)

Checks if the given hint requires a refactoring.

Parameters:

rule - The applied Rule.

goal - The Goal.

hint - The hint to check.

Returns:

true perform refactoring, false do not perform refactoring.

refactoreLabels

public void refactoreLabels(TermLabelState state,
                            Services services,
                            PosInOccurrence applicationPosInOccurrence,
                            Term applicationTerm,
                            Rule rule,
                            Goal goal,
                            java.lang.Object hint,
                            Term tacletTerm,
                            Term term,
                            java.util.List<TermLabel> labels)

This method is used to refactor the labels of the given Term.

Specified by:

refactoreLabels in interface TermLabelRefactoring

Parameters:

state - The TermLabelState of the current rule application.

services - The Services used by the Proof on which a Rule is applied right now.

applicationPosInOccurrence - The PosInOccurrence in the previous Sequent which defines the Term that is rewritten.

applicationTerm - The Term defined by the PosInOccurrence in the previous Sequent.

rule - The Rule which is applied.

goal - The optional Goal on which the Term to create will be used.

hint - An optional hint passed from the active rule to describe the term which should be created.

tacletTerm - The optional taclet Term.

term - The Term which is now refactored.

labels - The new labels the Term will have after the refactoring.

refactorSpecificationApplication

protected void refactorSpecificationApplication(Term term,
                                                Goal goal,
                                                Services services,
                                                java.util.List<TermLabel> labels,
                                                java.lang.Object hint)

Refactors a specification application.

Parameters:

term - The Term which is now refactored.

goal - The optional Goal on which the Term to create will be used.

services - The Services used by the Proof on which a Rule is applied right now.

labels - The new labels the Term will have after the refactoring.

refactorInCaseOfNewIdRequired

protected void refactorInCaseOfNewIdRequired(TermLabelState state,
                                             Goal goal,
                                             Term term,
                                             Services services,
                                             java.util.List<TermLabel> labels)

Refactors in case that the inner most label needs a new ID.

Parameters:

state - The TermLabelState of the current rule application.

goal - The optional Goal on which the Term to create will be used.

term - The Term which is now refactored.

services - The Services used by the Proof on which a Rule is applied right now.

labels - The new labels the Term will have after the refactoring.

refactorBewlowUpdates

protected void refactorBewlowUpdates(PosInOccurrence applicationPosInOccurrence,
                                     Term term,
                                     java.util.List<TermLabel> labels)

Refactors the Term below its update.

Parameters:

applicationPosInOccurrence - The PosInOccurrence in the previous Sequent which defines the Term that is rewritten.

term - The Term which is now refactored.

labels - The new labels the Term will have after the refactoring.

refactorSequentFormulas

protected void refactorSequentFormulas(TermLabelState state,
                                       Services services,
                                       Term term,
                                       java.util.List<TermLabel> labels)

Refactors the specified SequentFormulas.

Parameters:

state - The TermLabelState of the current rule application.

services - The Services used by the Proof on which a Rule is applied right now.

term - The Term which is now refactored.

labels - The new labels the Term will have after the refactoring.

refactorSubstitution

protected void refactorSubstitution(Term term,
                                    Term tacletTerm,
                                    java.util.List<TermLabel> labels)

Refactors the given Term after a substitiution.

Parameters:

term - The Term to refactor.

tacletTerm - The taclet Term which provides additional labels to be merged with the other Term.

labels - The new labels the Term will have after the refactoring.

isInnerMostParentRefactored

public static boolean isInnerMostParentRefactored(TermLabelState state,
                                                  Goal goal)

Checks if the inner most parent was already refactored on the given Goal.

Parameters:

state - The TermLabelState to read from.

goal - The Goal to check.

Returns:

true already refactored, false not refactored yet.

setInnerMostParentRefactored

public static void setInnerMostParentRefactored(TermLabelState state,
                                                Goal goal,
                                                boolean refactored)

Defines if the inner most parent was already refactored on the given Goal.

Parameters:

state - The TermLabelState to read from.

goal - The Goal to check.

refactored - true already refactored, false not refactored yet.

isUpdateRefactroingRequired

public static boolean isUpdateRefactroingRequired(TermLabelState state)

Checks if a refactoring below the updates is required.

Parameters:

state - The TermLabelState to read from.

Returns:

true refactoring required, false refactoring is not required.

setUpdateRefactroingRequired

public static void setUpdateRefactroingRequired(TermLabelState state,
                                                boolean required)

Defines if a refactoring below the updates is required.

Parameters:

state - The TermLabelState to modify.

required - true refactoring required, false refactoring is not required.

isParentRefactroingRequired

public static boolean isParentRefactroingRequired(TermLabelState state)

Checks if a refactoring of parents is required.

Parameters:

state - The TermLabelState to read from.

Returns:

true refactoring required, false refactoring is not required.

setParentRefactroingRequired

public static void setParentRefactroingRequired(TermLabelState state,
                                                boolean required)

Defines if a refactoring of parents is required.

Parameters:

state - The TermLabelState to modify.

required - true refactoring required, false refactoring is not required.

containsSequentFormulasToRefactor

public static boolean containsSequentFormulasToRefactor(TermLabelState state)

Checks if SequentFormulas to refactor are specified.

Parameters:

state - The TermLabelState to read from.

Returns:

true at least one SequentFormula needs to be refactored, false refactoring is not required.

getSequentFormulasToRefactor

public static java.util.Set<SequentFormula> getSequentFormulasToRefactor(TermLabelState state)

Returns the SequentFormulas to refactor.

Parameters:

state - The TermLabelState to read from.

Returns:

The SequentFormulas to refactor.

addSequentFormulaToRefactor

public static void addSequentFormulaToRefactor(TermLabelState state,
                                               SequentFormula sf)

Adds the given SequentFormula for refactoring purpose.

Parameters:

state - The TermLabelState to modify.

sf - The SequentFormula to add.