Package | Description |
---|---|
de.uka.ilkd.key.logic.label | |
de.uka.ilkd.key.rule.label |
Modifier and Type | Method and Description |
---|---|
ImmutableList<TermLabelUpdate> |
TermLabelManager.TermLabelConfiguration.getTermLabelUpdates()
Returns the
TermLabelUpdate instances. |
Modifier and Type | Method and Description |
---|---|
protected void |
TermLabelManager.performUpdater(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Term modalityTerm,
Rule rule,
RuleApp ruleApp,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
ImmutableList<TermLabelUpdate> updater,
java.util.Set<TermLabel> newLabels)
Performs the given child and grandchild
TermLabelUpdate instances. |
Constructor and Description |
---|
TermLabelConfiguration(Name termLabelName,
TermLabelFactory<?> factory,
ImmutableList<TermLabelPolicy> applicationTermPolicies,
ImmutableList<TermLabelPolicy> modalityTermPolicies,
ImmutableList<ChildTermLabelPolicy> directChildTermLabelPolicies,
ImmutableList<ChildTermLabelPolicy> childAndGrandchildTermLabelPolicies,
ImmutableList<TermLabelUpdate> termLabelUpdates,
ImmutableList<TermLabelRefactoring> termLabelRefactorings,
TermLabelMerger termLabelMerger)
Constructor.
|
Modifier and Type | Class and Description |
---|---|
class |
BlockContractValidityTermLabelUpdate
Makes sure that
BlockContractValidityTermLabel is introduced
when a BlockContractInternalRule is applied. |
class |
FormulaTermLabelUpdate
The
TermLabelUpdate used to label predicates with a
FormulaTermLabel of add clauses which were not labeled before. |
class |
LoopBodyTermLabelUpdate
Makes sure that
SymbolicExecutionUtil.LOOP_BODY_LABEL is introduced
when a WhileInvariantRule is applied. |
class |
LoopInvariantNormalBehaviorTermLabelUpdate
Makes sure that
SymbolicExecutionUtil.LOOP_INVARIANT_NORMAL_BEHAVIOR_LABEL is introduced
when a WhileInvariantRule is applied. |
class |
SymbolicExecutionTermLabelUpdate
Makes sure that the ID of
SymbolicExecutionTermLabel s is increased
when a WhileInvariantRule is applied. |
Copyright © 2003-2019 The KeY-Project.