public interface TermLabelRefactoring extends RuleSpecificTask
A TermLabelRefactoring
is used by
TermLabelManager#refactorGoal(TermLabelState, Services, PosInOccurrence,
Term, Rule, Goal, Term)
to refactor the labels of each visited Term
.
For more information about TermLabel
s and how they are maintained
during prove read the documentation of interface TermLabel
.
TermLabel
,
TermLabelManager
Modifier and Type | Interface and Description |
---|---|
static class |
TermLabelRefactoring.RefactoringScope
Possible refactoring scopes.
|
Modifier and Type | Method and Description |
---|---|
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 . |
void |
refactorLabels(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 . |
static boolean |
shouldRefactorOnBuiltInRule(Rule rule,
Goal goal,
java.lang.Object hint)
Determines whether any refatorings should be applied on an application of the given
BuiltInRule . |
getSupportedRuleNames
static boolean shouldRefactorOnBuiltInRule(Rule rule, Goal goal, java.lang.Object hint)
BuiltInRule
.
If you perform refactorings despite this method returning false, KeY will throw an exception
because the formula that contains the modality in which the contract was applied does not
have a FormulaTag.rule
- the rule being applied.goal
- the goal on which the rule is being applied.hint
- an optional hint passed from the active rule to describe the term which
should be created.TermLabelRefactoring.RefactoringScope defineRefactoringScope(TermLabelState state, Services services, PosInOccurrence applicationPosInOccurrence, Term applicationTerm, Rule rule, Goal goal, java.lang.Object hint, Term tacletTerm)
TermLabelRefactoring.RefactoringScope
.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
.TermLabelRefactoring.RefactoringScope
.void refactorLabels(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)
Term
.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.Copyright © 2003-2019 The KeY-Project.