de.uka.ilkd.key.rule.label

Interface TermLabelUpdate

All Superinterfaces:

RuleSpecificTask

All Known Implementing Classes:

BlockContractValidityTermLabelUpdate, FormulaTermLabelUpdate, LoopBodyTermLabelUpdate, LoopInvariantNormalBehaviorTermLabelUpdate, SymbolicExecutionTermLabelUpdate

public interface TermLabelUpdate
extends RuleSpecificTask

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 TermLabels which will be added to the new Term.

For more information about TermLabels and how they are maintained during prove read the documentation of interface TermLabel.

Author:

Martin Hentschel

See Also:

TermLabel, TermLabelManager

Method Summary

Modifier and Type

Method and Description

void

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) This method can freely add, remove or sort the given TermLabel which will be added to the new Term.

Methods inherited from interface de.uka.ilkd.key.rule.label.RuleSpecificTask

getSupportedRuleNames

Method Detail

updateLabels

void 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)

This method can freely add, remove or sort the given TermLabel which will be added to the new Term.

Parameters:

state - The TermLabelState of the current rule application. return true keep TermLabel and add it to the new Term. false drop TermLabel and do not need it to the new Term.

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.

modalityTerm - The optional modality Term.

rule - The Rule which is applied.

ruleApp - The RuleApp which is currently performed.

hint - An optional hint passed from the active rule to describe the term which should be created.

tacletTerm - The optional Term in the taclet which is responsible to instantiate the new Term for the new proof node or null in case of built in rules.

newTermOp - The new Operator of the Term to create.

newTermSubs - The optional children of the Term to create.

newTermBoundVars - The optional QuantifiableVariables of the Term to create.

newTermJavaBlock - The optional JavaBlock of the Term to create.

labels - The Set of TermLabels to modify.