Package | Description |
---|---|
de.uka.ilkd.key.logic.label | |
de.uka.ilkd.key.rule.label |
Class and Description |
---|
ChildTermLabelPolicy
A
ChildTermLabelPolicy is used by
TermLabelManager#instantiateLabels(
TermLabelState, Services, PosInOccurrence, Term, Term, Rule, Goal,
Object, Term, Operator, ImmutableArray, ImmutableArray, JavaBlock)
to decide for each TermLabel on a child or grandchild of the
application Term if it should be re-added to the new Term
or not. |
TermLabelMerger
A
TermLabelMerger is used by
TermLabelManager.mergeLabels(Services, de.uka.ilkd.key.logic.SequentChangeInfo)
to merge TermLabel s in case a SequentFormula was
rejected to be added to the resulting Sequent . |
TermLabelPolicy
A
TermLabelPolicy is used by
TermLabelManager#instantiateLabels(
TermLabelState, Services, PosInOccurrence, Term, Term, Rule, Goal,
Object, Term, Operator, ImmutableArray, ImmutableArray, JavaBlock)
to decide for each TermLabel of an old Term if it
should be re-added to the new Term or not. |
TermLabelRefactoring
A
TermLabelRefactoring is used by
TermLabelManager#refactorGoal(TermLabelState, Services, PosInOccurrence,
Term, Rule, Goal, Term)
to refactor the labels of each visited Term . |
TermLabelUpdate
A
TermLabelUpdate is used by
TermLabelManager#instantiateLabels(
TermLabelState, Services, PosInOccurrence, Term, Term, Rule, Goal,
Object, Term, Operator, ImmutableArray, ImmutableArray, JavaBlock)
to add or remove maintained TermLabel s which will be added to the new Term . |
Class and Description |
---|
RuleSpecificTask
Instances of this class provides functionality only if a supported
rule is active.
|
TermLabelMerger
A
TermLabelMerger is used by
TermLabelManager.mergeLabels(Services, de.uka.ilkd.key.logic.SequentChangeInfo)
to merge TermLabel s in case a SequentFormula was
rejected to be added to the resulting Sequent . |
TermLabelPolicy
A
TermLabelPolicy is used by
TermLabelManager#instantiateLabels(
TermLabelState, Services, PosInOccurrence, Term, Term, Rule, Goal,
Object, Term, Operator, ImmutableArray, ImmutableArray, JavaBlock)
to decide for each TermLabel of an old Term if it
should be re-added to the new Term or not. |
TermLabelRefactoring
A
TermLabelRefactoring is used by
TermLabelManager#refactorGoal(TermLabelState, Services, PosInOccurrence,
Term, Rule, Goal, Term)
to refactor the labels of each visited Term . |
TermLabelRefactoring.RefactoringScope
Possible refactoring scopes.
|
TermLabelUpdate
A
TermLabelUpdate is used by
TermLabelManager#instantiateLabels(
TermLabelState, Services, PosInOccurrence, Term, Term, Rule, Goal,
Object, Term, Operator, ImmutableArray, ImmutableArray, JavaBlock)
to add or remove maintained TermLabel s which will be added to the new Term . |
Copyright © 2003-2019 The KeY-Project.