Package | Description |
---|---|
de.uka.ilkd.key.informationflow.rule.executor | |
de.uka.ilkd.key.logic.label | |
de.uka.ilkd.key.rule |
This package contains classes for implementing rules.
|
de.uka.ilkd.key.rule.executor.javadl | |
de.uka.ilkd.key.rule.label | |
de.uka.ilkd.key.rule.metaconstruct |
contains classes representing the meta constructs of
Taclet s. |
de.uka.ilkd.key.strategy.quantifierHeuristics |
Modifier and Type | Method and Description |
---|---|
protected void |
InfFlowContractAppTacletExecutor.addToAntec(Semisequent semi,
TermLabelState termLabelState,
Taclet.TacletLabelHint labelHint,
SequentChangeInfo currentSequent,
PosInOccurrence pos,
PosInOccurrence applicationPosInOccurrence,
MatchConditions matchCond,
Goal goal,
RuleApp tacletApp,
Services services) |
Modifier and Type | Method and Description |
---|---|
protected TermLabelManager.RefactoringsContainer |
TermLabelManager.computeRefactorings(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm)
Computes the
TermLabelRefactoring to consider. |
static ImmutableArray<TermLabel> |
TermLabelManager.instantiateLabels(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Rule rule,
RuleApp ruleApp,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
ImmutableArray<TermLabel> newTermOriginalLabels)
|
ImmutableArray<TermLabel> |
TermLabelManager.instantiateLabels(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
RuleApp ruleApp,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
ImmutableArray<TermLabel> newTermOriginalLabels)
|
static ImmutableArray<TermLabel> |
TermLabelManager.instantiateLabels(TermLabelState state,
Services services,
Term applicationTerm,
PosInOccurrence applicationPosInOccurrence,
Rule rule,
RuleApp ruleApp,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
ImmutableArray<TermLabel> newTermOriginalLabels)
|
static Term |
TermLabelManager.label(Services services,
TermLabelState state,
PosInOccurrence applicationPosInOccurrence,
Rule rule,
RuleApp ruleApp,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Term newTerm)
Computes the
TermLabel s for the new Term via
TermLabelManager.instantiateLabels(TermLabelState, Services, PosInOccurrence, Term, Rule, RuleApp,
Goal, Object, Term, Operator, ImmutableArray, ImmutableArray,
JavaBlock, ImmutableArray)
and refactors the labels below the new Term in addition via
TermLabelManager.refactorTerm(TermLabelState, Services, PosInOccurrence, Term, Goal, Object,
Rule, Term) . |
static Term |
TermLabelManager.label(Services services,
TermLabelState state,
Term applicationTerm,
PosInOccurrence applicationPosInOccurrence,
Rule rule,
RuleApp ruleApp,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Term newTerm)
Computes the
TermLabel s for the new Term via
TermLabelManager.instantiateLabels(TermLabelState, Services, PosInOccurrence, Term, Rule, RuleApp,
Goal, Object, Term, Operator, ImmutableArray, ImmutableArray,
JavaBlock, ImmutableArray)
and refactors the labels below the new Term in addition via
TermLabelManager.refactorTerm(TermLabelState, Services, PosInOccurrence, Term, Goal, Object,
Rule, Term) . |
Term |
TermLabelManager.label(TermLabelState state,
Services services,
Term applicationTerm,
PosInOccurrence applicationPosInOccurrence,
Rule rule,
RuleApp ruleApp,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Term newTerm)
Computes the
TermLabel s for the new Term via
TermLabelManager.instantiateLabels(TermLabelState, Services, PosInOccurrence, Term, Rule, RuleApp,
Goal, Object, Term, Operator, ImmutableArray, ImmutableArray,
JavaBlock, ImmutableArray)
and refactors the labels below the new Term in addition via
TermLabelManager.refactorTerm(TermLabelState, Services, PosInOccurrence, Term, Goal, Object,
Rule, Term) . |
protected ImmutableArray<TermLabel> |
TermLabelManager.performRefactoring(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Term term,
ImmutableList<TermLabelRefactoring> activeRefactorings)
Computes the new labels as part of the refactoring for the given
Term . |
protected void |
TermLabelManager.performTermLabelPolicies(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
ImmutableArray<TermLabel> newTermOriginalLabels,
java.util.Map<Name,TermLabelPolicy> policies,
java.util.Set<TermLabel> newLabels)
Performs the given
TermLabelPolicy instances. |
protected void |
TermLabelManager.performTermLabelPolicies(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
ImmutableArray<TermLabel> newTermOriginalLabels,
java.util.Map<Name,TermLabelPolicy> policies,
java.util.Set<TermLabel> newLabels,
TermLabel label)
Performs the given
TermLabelPolicy instances. |
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. |
protected Term |
TermLabelManager.refactorApplicationTerm(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
TermLabelManager.RefactoringsContainer refactorings,
TermFactory tf)
Refactors the labels of the application term.
|
static void |
TermLabelManager.refactorGoal(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm)
Refactors all labels in the complete
Sequent . |
void |
TermLabelManager.refactorGoal(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm)
Refactors all labels in the complete
Sequent . |
protected Term |
TermLabelManager.refactorLabelsRecursive(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Term term,
ImmutableList<TermLabelRefactoring> activeRefactorings)
|
protected void |
TermLabelManager.refactorSemisequent(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Semisequent semisequent,
boolean inAntec,
ImmutableList<TermLabelRefactoring> activeRefactorings)
Performs a
TermLabel refactoring on the given Semisequent . |
static void |
TermLabelManager.refactorSequent(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm)
Refactors all labels in the complete
Sequent . |
void |
TermLabelManager.refactorSequent(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm)
Refactors all labels in the complete
Sequent . |
Term |
TermLabelManager.refactorSequentFormula(TermLabelState state,
Services services,
Term sequentFormula,
PosInOccurrence applicationPosInOccurrence,
Goal goal,
java.lang.Object hint,
Rule rule,
Term tacletTerm)
|
static Term |
TermLabelManager.refactorSequentFormula(TermLabelState state,
Services services,
Term sequentFormula,
PosInOccurrence applicationPosInOccurrence,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm)
|
Term |
TermLabelManager.refactorTerm(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Goal goal,
java.lang.Object hint,
Rule rule,
Term tacletTerm)
Refactors all labels in the given application
Term . |
static Term |
TermLabelManager.refactorTerm(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm)
Refactors all labels in the complete
Sequent . |
protected Term |
TermLabelManager.replaceTerm(TermLabelState state,
PosInOccurrence pio,
Term newTerm,
TermFactory tf,
ImmutableList<TermLabelRefactoring> parentRefactorings,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm)
Replaces the
Term at the specified PosInOccurrence . |
Modifier and Type | Field and Description |
---|---|
protected TermLabelState |
SyntacticalReplaceVisitor.termLabelState |
TermLabelState |
AbstractLoopInvariantRule.LoopInvariantInformation.termLabelState
The
TermLabelState . |
Modifier and Type | Method and Description |
---|---|
SequentFormula |
RewriteTaclet.getRewriteResult(Goal goal,
TermLabelState termLabelState,
Services services,
TacletApp app) |
Constructor and Description |
---|
GoalsConfigurator(AbstractAuxiliaryContractBuiltInRuleApp application,
TermLabelState termLabelState,
AbstractAuxiliaryContractRule.Instantiation instantiation,
java.util.List<Label> labels,
AuxiliaryContract.Variables variables,
PosInOccurrence occurrence,
Services services,
AbstractAuxiliaryContractRule rule) |
LoopInvariantInformation(Goal goal,
Services services,
AbstractLoopInvariantRule.Instantiation inst,
LoopInvariantBuiltInRuleApp ruleApp,
ImmutableList<Goal> goals,
TermLabelState termLabelState,
Term invTerm,
Term variantPO,
Term reachableState,
Term anonUpdate,
Term wellFormedAnon,
Term uAnonInv,
Term frameCondition,
Term[] uBeforeLoopDefAnonVariant,
ImmutableList<AbstractLoopInvariantRule.AnonUpdateData> anonUpdateData)
Creates a new
AbstractLoopInvariantRule.LoopInvariantInformation object. |
SyntacticalReplaceVisitor(TermLabelState termLabelState,
Taclet.TacletLabelHint labelHint,
PosInOccurrence applicationPosInOccurrence,
Goal goal,
Rule rule,
RuleApp ruleApp,
Services services,
TermBuilder termBuilder) |
SyntacticalReplaceVisitor(TermLabelState termLabelState,
Taclet.TacletLabelHint labelHint,
PosInOccurrence applicationPosInOccurrence,
SVInstantiations svInst,
Goal goal,
Rule rule,
RuleApp ruleApp,
Services services)
constructs a term visitor replacing any occurrence of a schemavariable found
in
svInst by its instantiation |
Modifier and Type | Method and Description |
---|---|
protected void |
TacletExecutor.addToAntec(Semisequent semi,
TermLabelState termLabelState,
Taclet.TacletLabelHint labelHint,
SequentChangeInfo currentSequent,
PosInOccurrence pos,
PosInOccurrence applicationPosInOccurrence,
MatchConditions matchCond,
Goal goal,
RuleApp tacletApp,
Services services)
adds SequentFormula to antecedent depending on
position information (if none is handed over it is added at the
head of the antecedent).
|
protected void |
TacletExecutor.addToSucc(Semisequent semi,
TermLabelState termLabelState,
Taclet.TacletLabelHint labelHint,
SequentChangeInfo currentSequent,
PosInOccurrence pos,
PosInOccurrence applicationPosInOccurrence,
MatchConditions matchCond,
Goal goal,
RuleApp ruleApp,
Services services)
adds SequentFormula to succedent depending on
position information (if none is handed over it is added at the
head of the succedent).
|
protected void |
RewriteTacletExecutor.applyAdd(Sequent add,
TermLabelState termLabelState,
SequentChangeInfo currentSequent,
PosInOccurrence whereToAdd,
PosInOccurrence posOfFind,
MatchConditions matchCond,
Goal goal,
RuleApp ruleApp,
Services services)
adds the sequent of the add part of the Taclet to the goal sequent
|
protected void |
SuccTacletExecutor.applyAdd(Sequent add,
TermLabelState termLabelState,
SequentChangeInfo currentSequent,
PosInOccurrence whereToAdd,
PosInOccurrence posOfFind,
MatchConditions matchCond,
Goal goal,
RuleApp ruleApp,
Services services)
applies the
add -expressions of taclet goal descriptions |
protected abstract void |
FindTacletExecutor.applyAdd(Sequent add,
TermLabelState termLabelState,
SequentChangeInfo currentSequent,
PosInOccurrence whereToAdd,
PosInOccurrence posOfFind,
MatchConditions matchCond,
Goal goal,
RuleApp ruleApp,
Services services)
applies the
add -expressions of taclet goal descriptions |
protected void |
AntecTacletExecutor.applyAdd(Sequent add,
TermLabelState termLabelState,
SequentChangeInfo currentSequent,
PosInOccurrence whereToAdd,
PosInOccurrence posOfFind,
MatchConditions matchCond,
Goal goal,
RuleApp ruleApp,
Services services)
applies the
add -expressions of taclet goal descriptions |
protected void |
NoFindTacletExecutor.applyAdd(TermLabelState termLabelState,
Sequent add,
SequentChangeInfo currentSequent,
Services services,
MatchConditions matchCond,
Goal goal,
RuleApp ruleApp)
adds the sequent of the add part of the Taclet to the goal sequent
|
protected void |
RewriteTacletExecutor.applyReplacewith(TacletGoalTemplate gt,
TermLabelState termLabelState,
SequentChangeInfo currentSequent,
PosInOccurrence posOfFind,
MatchConditions matchCond,
Goal goal,
RuleApp ruleApp,
Services services)
applies the
replacewith -expression of taclet goal descriptions |
protected void |
SuccTacletExecutor.applyReplacewith(TacletGoalTemplate gt,
TermLabelState termLabelState,
SequentChangeInfo currentSequent,
PosInOccurrence posOfFind,
MatchConditions matchCond,
Goal goal,
RuleApp ruleApp,
Services services)
applies the
replacewith -expression of taclet goal descriptions |
protected abstract void |
FindTacletExecutor.applyReplacewith(TacletGoalTemplate gt,
TermLabelState termLabelState,
SequentChangeInfo currentSequent,
PosInOccurrence posOfFind,
MatchConditions matchCond,
Goal goal,
RuleApp ruleApp,
Services services)
applies the
replacewith -expression of taclet goal descriptions |
protected void |
AntecTacletExecutor.applyReplacewith(TacletGoalTemplate gt,
TermLabelState termLabelState,
SequentChangeInfo currentSequent,
PosInOccurrence posOfFind,
MatchConditions matchCond,
Goal goal,
RuleApp ruleApp,
Services services)
applies the
replacewith -expression of taclet goal descriptions |
SequentFormula |
RewriteTacletExecutor.getRewriteResult(Goal goal,
TermLabelState termLabelState,
Services services,
TacletApp app) |
protected ImmutableList<SequentFormula> |
TacletExecutor.instantiateSemisequent(Semisequent semi,
TermLabelState termLabelState,
Taclet.TacletLabelHint labelHint,
PosInOccurrence applicationPosInOccurrence,
MatchConditions matchCond,
Goal goal,
RuleApp tacletApp,
Services services)
instantiates the given semisequent with the instantiations found in
Matchconditions
|
protected void |
TacletExecutor.replaceAtPos(Semisequent semi,
TermLabelState termLabelState,
SequentChangeInfo currentSequent,
PosInOccurrence pos,
MatchConditions matchCond,
Taclet.TacletLabelHint labelHint,
Goal goal,
RuleApp ruleApp,
Services services)
replaces the constrained formula at the given position with the first
formula in the given semisequent and adds possible other formulas of the
semisequent starting at the position
|
protected Term |
TacletExecutor.syntacticalReplace(Term term,
TermLabelState termLabelState,
Taclet.TacletLabelHint labelHint,
PosInOccurrence applicationPosInOccurrence,
MatchConditions mc,
Goal goal,
RuleApp ruleApp,
Services services)
a new term is created by replacing variables of term whose replacement is
found in the given SVInstantiations
|
Modifier and Type | Method and Description |
---|---|
static void |
FormulaTermLabelRefactoring.addSequentFormulaToRefactor(TermLabelState state,
SequentFormula sf)
Adds the given
SequentFormula for refactoring purpose. |
static boolean |
FormulaTermLabelRefactoring.containsSequentFormulasToRefactor(TermLabelState state)
Checks if
SequentFormula s to refactor are specified. |
TermLabelRefactoring.RefactoringScope |
TermLabelRefactoring.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 . |
TermLabelRefactoring.RefactoringScope |
OriginTermLabelRefactoring.defineRefactoringScope(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm) |
TermLabelRefactoring.RefactoringScope |
FormulaTermLabelRefactoring.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 . |
TermLabelRefactoring.RefactoringScope |
RemoveInCheckBranchesTermLabelRefactoring.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> |
FormulaTermLabelRefactoring.getSequentFormulasToRefactor(TermLabelState state)
Returns the
SequentFormula s to refactor. |
static boolean |
FormulaTermLabelRefactoring.isInnerMostParentRefactored(TermLabelState state,
Goal goal)
Checks if the inner most parent was already refactored on the given
Goal . |
static boolean |
FormulaTermLabelRefactoring.isParentRefactroingRequired(TermLabelState state)
Checks if a refactoring of parents is required.
|
static boolean |
FormulaTermLabelRefactoring.isUpdateRefactroingRequired(TermLabelState state)
Checks if a refactoring below the updates is required.
|
TermLabel |
OriginTermLabelPolicy.keepLabel(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
ImmutableArray<TermLabel> newTermOriginalLabels,
TermLabel label) |
TermLabel |
TermLabelPolicy.keepLabel(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
ImmutableArray<TermLabel> newTermOriginalLabels,
TermLabel label)
|
TermLabel |
PerpetualTermLabelPolicy.keepLabel(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
ImmutableArray<TermLabel> newTermOriginalLabels,
TermLabel label) |
TermLabel |
StayOnOperatorTermLabelPolicy.keepLabel(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
ImmutableArray<TermLabel> newTermOriginalLabels,
TermLabel label)
|
TermLabel |
StayOnFormulaTermLabelPolicy.keepLabel(TermLabelState state,
Services services,
PosInOccurrence applicationPosInOccurrence,
Term applicationTerm,
Rule rule,
Goal goal,
java.lang.Object hint,
Term tacletTerm,
Operator newTermOp,
ImmutableArray<Term> newTermSubs,
ImmutableArray<QuantifiableVariable> newTermBoundVars,
JavaBlock newTermJavaBlock,
ImmutableArray<TermLabel> newTermOriginalLabels,
TermLabel label)
|
protected void |
FormulaTermLabelRefactoring.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 |
TermLabelRefactoring.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 . |
void |
OriginTermLabelRefactoring.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) |
void |
FormulaTermLabelRefactoring.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 . |
void |
RemoveInCheckBranchesTermLabelRefactoring.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 |
FormulaTermLabelRefactoring.refactorSequentFormulas(TermLabelState state,
Services services,
Term term,
java.util.List<TermLabel> labels)
Refactors the specified
SequentFormula s. |
static void |
FormulaTermLabelRefactoring.setInnerMostParentRefactored(TermLabelState state,
Goal goal,
boolean refactored)
Defines if the inner most parent was already refactored on the given
Goal . |
static void |
FormulaTermLabelRefactoring.setParentRefactroingRequired(TermLabelState state,
boolean required)
Defines if a refactoring of parents is required.
|
static void |
FormulaTermLabelRefactoring.setUpdateRefactroingRequired(TermLabelState state,
boolean required)
Defines if a refactoring below the updates is required.
|
void |
TermLabelUpdate.updateLabels(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,
java.util.Set<TermLabel> labels)
|
void |
FormulaTermLabelUpdate.updateLabels(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,
java.util.Set<TermLabel> labels)
|
void |
LoopBodyTermLabelUpdate.updateLabels(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,
java.util.Set<TermLabel> labels)
|
void |
BlockContractValidityTermLabelUpdate.updateLabels(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,
java.util.Set<TermLabel> labels)
|
void |
SymbolicExecutionTermLabelUpdate.updateLabels(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,
java.util.Set<TermLabel> labels)
|
void |
LoopInvariantNormalBehaviorTermLabelUpdate.updateLabels(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,
java.util.Set<TermLabel> labels)
|
Modifier and Type | Method and Description |
---|---|
Term |
WhileInvariantTransformer.transform(TermLabelState termLabelState,
Rule rule,
RuleApp ruleApp,
Goal goal,
Sequent applicationSequent,
PosInOccurrence applicationPos,
Term initialPost,
Term invariantFramingTermination,
SVInstantiations svInst,
Services services)
calculates the resulting term.
|
Constructor and Description |
---|
ConstraintAwareSyntacticalReplaceVisitor(TermLabelState termLabelState,
Services services,
Constraint metavariableInst,
PosInOccurrence applicationPosInOccurrence,
Rule rule,
RuleApp ruleApp,
Taclet.TacletLabelHint labelHint,
Goal goal) |
Copyright © 2003-2019 The KeY-Project.