public class FormulaTermLabelRefactoring extends java.lang.Object implements TermLabelRefactoring
TermLabelRefactoring
used to label predicates with a
FormulaTermLabel
on applied loop invariants or operation contracts.TermLabelRefactoring.RefactoringScope
Constructor and Description |
---|
FormulaTermLabelRefactoring() |
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
SequentFormula s 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
SequentFormula s to refactor. |
ImmutableList<Name> |
getSupportedRuleNames()
Returns the supported rule
Name s 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. |
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.
|
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 . |
protected void |
refactorSequentFormulas(TermLabelState state,
Services services,
Term term,
java.util.List<TermLabel> labels)
Refactors the specified
SequentFormula s. |
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.
|
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
shouldRefactorOnBuiltInRule
public ImmutableList<Name> getSupportedRuleNames()
Name
s or null
or an empty
list if all rules are supported.getSupportedRuleNames
in interface RuleSpecificTask
Name
s or null
/empty list if all rules are supported.public TermLabelRefactoring.RefactoringScope defineRefactoringScope(TermLabelState state, Services services, PosInOccurrence applicationPosInOccurrence, Term applicationTerm, Rule rule, Goal goal, java.lang.Object hint, Term tacletTerm)
TermLabelRefactoring.RefactoringScope
.defineRefactoringScope
in interface TermLabelRefactoring
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
.protected boolean shouldRefactorSpecificationApplication(Rule rule, Goal goal, java.lang.Object hint)
public 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
.refactorLabels
in interface TermLabelRefactoring
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.protected void refactorSpecificationApplication(Term term, Goal goal, Services services, java.util.List<TermLabel> labels, java.lang.Object hint)
protected void refactorInCaseOfNewIdRequired(TermLabelState state, Goal goal, Term term, Services services, java.util.List<TermLabel> labels)
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.protected void refactorBewlowUpdates(PosInOccurrence applicationPosInOccurrence, Term term, java.util.List<TermLabel> labels)
Term
below its update.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.protected void refactorSequentFormulas(TermLabelState state, Services services, Term term, java.util.List<TermLabel> labels)
SequentFormula
s.protected void refactorSubstitution(Term term, Term tacletTerm, java.util.List<TermLabel> labels)
Term
after a substitiution.public static boolean isInnerMostParentRefactored(TermLabelState state, Goal goal)
Goal
.state
- The TermLabelState
to read from.goal
- The Goal
to check.true
already refactored, false
not refactored yet.public static void setInnerMostParentRefactored(TermLabelState state, Goal goal, boolean refactored)
Goal
.state
- The TermLabelState
to read from.goal
- The Goal
to check.refactored
- true
already refactored, false
not refactored yet.public static boolean isUpdateRefactroingRequired(TermLabelState state)
state
- The TermLabelState
to read from.true
refactoring required, false
refactoring is not required.public static void setUpdateRefactroingRequired(TermLabelState state, boolean required)
state
- The TermLabelState
to modify.required
- true
refactoring required, false
refactoring is not required.public static boolean isParentRefactroingRequired(TermLabelState state)
state
- The TermLabelState
to read from.true
refactoring required, false
refactoring is not required.public static void setParentRefactroingRequired(TermLabelState state, boolean required)
state
- The TermLabelState
to modify.required
- true
refactoring required, false
refactoring is not required.public static boolean containsSequentFormulasToRefactor(TermLabelState state)
SequentFormula
s to refactor are specified.state
- The TermLabelState
to read from.true
at least one SequentFormula
needs to be refactored, false
refactoring is not required.public static java.util.Set<SequentFormula> getSequentFormulasToRefactor(TermLabelState state)
SequentFormula
s to refactor.state
- The TermLabelState
to read from.SequentFormula
s to refactor.public static void addSequentFormulaToRefactor(TermLabelState state, SequentFormula sf)
SequentFormula
for refactoring purpose.state
- The TermLabelState
to modify.sf
- The SequentFormula
to add.Copyright © 2003-2019 The KeY-Project.