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
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 SequentFormula s
(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 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. |
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
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.
|
private static final java.lang.String INNER_MOST_PARENT_REFACTORED_PREFIX
TermLabelState
to store that the inner most
label was already refactored on a given Goal
.private static final java.lang.String UPDATE_REFACTORING_REQUIRED
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
private static final java.lang.String PARENT_REFACTORING_REQUIRED
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
private static final java.lang.String SEQUENT_FORMULA_REFACTORING_REQUIRED
TermLabelState
by the FormulaTermLabelUpdate
to indicate that a refactoring of specified SequentFormula
s
(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
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 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)
Term
.refactoreLabels
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.