de.uka.ilkd.key.rule.label (KeY API Documentation)

Interface Summary
Interface	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.
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`.
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 Summary
Class	Description
BlockContractValidityTermLabelUpdate	Makes sure that `BlockContractValidityTermLabel` is introduced when a `BlockContractInternalRule` is applied.
FormulaTermLabelMerger	The `TermLabelMerger` used to merge `FormulaTermLabel`s.
FormulaTermLabelRefactoring	The `TermLabelRefactoring` used to label predicates with a `FormulaTermLabel` on applied loop invariants or operation contracts.
FormulaTermLabelUpdate	The `TermLabelUpdate` used to label predicates with a `FormulaTermLabel` of add clauses which were not labeled before.
LoopBodyTermLabelUpdate	Makes sure that `SymbolicExecutionUtil.LOOP_BODY_LABEL` is introduced when a `WhileInvariantRule` is applied.
LoopInvariantNormalBehaviorTermLabelUpdate	Makes sure that `SymbolicExecutionUtil.LOOP_INVARIANT_NORMAL_BEHAVIOR_LABEL` is introduced when a `WhileInvariantRule` is applied.
RemoveInCheckBranchesTermLabelRefactoring	This `TermLabelRefactoring` removes the supported `TermLabel` in check branches.
StayOnFormulaTermLabelPolicy	This `TermLabelPolicy` maintains a `FormulaTermLabel` on predicates.
StayOnOperatorTermLabelPolicy	This `TermLabelPolicy` maintains a `TermLabel` as long the new `Term` has the same `Operator` as the previous best matching `Term` from which it was created.
SymbolicExecutionTermLabelUpdate	Makes sure that the ID of `SymbolicExecutionTermLabel`s is increased when a `WhileInvariantRule` is applied.

Enum Summary
Enum Description

TermLabelRefactoring.RefactoringScope
Possible refactoring scopes.

Package de.uka.ilkd.key.rule.label