Package | Description |
---|---|
de.uka.ilkd.key.control | |
de.uka.ilkd.key.logic |
provides a representation for the term and sequent
structure.
|
de.uka.ilkd.key.logic.label | |
de.uka.ilkd.key.logic.op |
contains the operators of
Term s. |
de.uka.ilkd.key.nparser.builder | |
de.uka.ilkd.key.pp |
This package contains pretty-printing functionality used by the GUI and for
saving proofs.
|
de.uka.ilkd.key.rule.inst |
contains classes for the instantiation of schema variables of
Taclet s. |
de.uka.ilkd.key.rule.label | |
de.uka.ilkd.key.rule.match.vm.instructions | |
de.uka.ilkd.key.smt.newsmt2 | |
de.uka.ilkd.key.speclang |
This package contains the specification language frontends of KeY.
|
de.uka.ilkd.key.speclang.njml |
This package provides the functionalities of parsing JML comments into KeY constructs.
|
de.uka.ilkd.key.strategy.termfeature | |
de.uka.ilkd.key.symbolic_execution.util |
Modifier and Type | Method and Description |
---|---|
boolean |
TermLabelVisibilityManager.contains(TermLabel label) |
Modifier and Type | Method and Description |
---|---|
TermLabel |
TermImpl.getLabel(Name termLabelName) |
TermLabel |
Term.getLabel(Name termLabelName)
|
Modifier and Type | Method and Description |
---|---|
ImmutableArray<TermLabel> |
TermImpl.getLabels() |
ImmutableArray<TermLabel> |
Term.getLabels()
returns list of labels attached to this term
|
Modifier and Type | Method and Description |
---|---|
Term |
TermBuilder.addLabel(Term term,
TermLabel label)
Adds a label to a term, removing any existing labels of the same type.
|
Term |
TermBuilder.addLabelToAllSubs(Term term,
TermLabel label)
Applies the label to the term and almost every (direct or indirect) sub-term recursively.
|
boolean |
TermImpl.containsLabel(TermLabel label) |
boolean |
Term.containsLabel(TermLabel label)
checks if the given label is attached to the term
|
Term |
TermFactory.createTerm(Operator op,
Term[] subs,
ImmutableArray<QuantifiableVariable> boundVars,
JavaBlock javaBlock,
TermLabel label) |
Term |
TermFactory.createTerm(Operator op,
Term[] subs,
TermLabel label) |
Term |
TermBuilder.label(Term term,
TermLabel label)
Applies a label to a term, removing any existing labels.
|
Modifier and Type | Method and Description |
---|---|
Term |
TermBuilder.addLabel(Term term,
ImmutableArray<TermLabel> labels)
Adds labels to a term, removing any existing labels of the same type.
|
Term |
TermBuilder.addLabelToAllSubs(Term term,
ImmutableArray<TermLabel> labels)
Applies the labels to the term and almost every (direct or indirect) sub-term recursively.
|
Term |
TermBuilder.apply(Term update,
Term target,
ImmutableArray<TermLabel> labels) |
Term |
TermFactory.createTerm(Operator op,
ImmutableArray<Term> subs,
ImmutableArray<QuantifiableVariable> boundVars,
JavaBlock javaBlock,
ImmutableArray<TermLabel> labels)
Master method for term creation.
|
Term |
TermFactory.createTerm(Operator op,
ImmutableArray<TermLabel> labels) |
Term |
TermFactory.createTerm(Operator op,
Term[] subs,
ImmutableArray<QuantifiableVariable> boundVars,
JavaBlock javaBlock,
ImmutableArray<TermLabel> labels) |
Term |
TermFactory.createTerm(Operator op,
Term[] subs,
ImmutableArray<TermLabel> labels) |
Term |
TermFactory.createTerm(Operator op,
Term sub,
ImmutableArray<TermLabel> labels) |
Term |
TermFactory.createTerm(Operator op,
Term sub1,
Term sub2,
ImmutableArray<TermLabel> labels) |
Term |
TermBuilder.imp(Term t1,
Term t2,
ImmutableArray<TermLabel> labels) |
Term |
TermBuilder.label(Term term,
ImmutableArray<TermLabel> labels)
Applies labels to a term, removing any existing labels.
|
Term |
TermBuilder.prog(Modality mod,
JavaBlock jb,
Term t,
ImmutableArray<TermLabel> labels) |
Modifier and Type | Class and Description |
---|---|
class |
SingletonLabelFactory<T extends TermLabel>
A factory for creating singleton
TermLabel . |
interface |
TermLabelFactory<T extends TermLabel>
A factory for creating TermLabel objects.
|
Modifier and Type | Class and Description |
---|---|
class |
BlockContractValidityTermLabel
Label attached to the modality of the validity branch of a block contract.
|
class |
FormulaTermLabel
Label attached to a predicates for instance in postconditions, loop invariants or precondition checks of applied operation contracts.
|
class |
OriginTermLabel
An
OriginTermLabel saves a term's origin in the JML specification
(OriginTermLabel.getOrigin() ) as well as the origins of all of its subterms and former
subterms (OriginTermLabel.getSubtermOrigins() ). |
class |
ParameterlessTermLabel
The Class
ParameterlessTermLabel can be used to define labels without parameters. |
class |
SymbolicExecutionTermLabel
Label attached to a symbolic execution thread.
|
Modifier and Type | Field and Description |
---|---|
static TermLabel |
ParameterlessTermLabel.ANON_HEAP_LABEL
Label attached to anonymisation heap function symbols as for instance
introduce in UseOperationContractRule or WhileInvariantRule.
|
static TermLabel |
ParameterlessTermLabel.IMPLICIT_SPECIFICATION_LABEL
Label attached to a term which is specified implicitly (by the JML specification).
|
static TermLabel |
ParameterlessTermLabel.LOOP_SCOPE_INDEX_LABEL
Label attached to loop scope index variables in
LoopScopeInvariantRule . |
static TermLabel |
ParameterlessTermLabel.POST_CONDITION_LABEL
Label attached to the post-condition.
|
static TermLabel |
ParameterlessTermLabel.SELECT_SKOLEM_LABEL
Label attached to skolem constants introduced by the rule pullOutSelect.
|
static TermLabel |
ParameterlessTermLabel.SELF_COMPOSITION_LABEL
Label attached to the post condition.
|
static TermLabel |
ParameterlessTermLabel.SHORTCUT_EVALUATION_LABEL
Label attached to a term with the logical operator '||' or
'&&' to distinguish from '|' or '&'
respectively.
|
static TermLabel |
ParameterlessTermLabel.UNDEFINED_VALUE_LABEL
Label attached to a term which denotes an undefined value.
|
Modifier and Type | Method and Description |
---|---|
static TermLabel |
TermLabelManager.findInnerMostParentLabel(PosInOccurrence pio,
Name termLabelName)
Searches the inner most
TermLabel wit the given Name in the parent hierarchy of the PosInOccurrence . |
TermLabel |
TermLabelManager.parseLabel(java.lang.String name,
java.util.List<java.lang.String> args,
TermServices services)
Get a term label for string parameters.
|
Modifier and Type | Method and Description |
---|---|
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)
|
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 . |
Modifier and Type | Method and Description |
---|---|
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. |
Modifier and Type | Method and Description |
---|---|
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)
|
protected void |
TermLabelManager.performChildAndGrandchildPolicies(TermServices 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,
java.util.Map<Name,ChildTermLabelPolicy> policies,
java.util.Set<TermLabel> newLabels)
Performs the given child and grandchild
ChildTermLabelPolicy instances. |
protected void |
TermLabelManager.performDirectChildPolicies(TermServices 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,
java.util.Map<Name,ChildTermLabelPolicy> policies,
java.util.Set<TermLabel> newLabels)
Performs the given direct
ChildTermLabelPolicy instances. |
protected void |
TermLabelManager.performTacletTerm(Term tacletTerm,
java.util.Set<TermLabel> newLabels)
|
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)
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.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. |
Modifier and Type | Class and Description |
---|---|
class |
TermLabelSV
A schema variable which matches term labels
|
Modifier and Type | Method and Description |
---|---|
TermLabel |
ExpressionBuilder.visitSingle_label(KeYParser.Single_labelContext ctx) |
Modifier and Type | Method and Description |
---|---|
ImmutableArray<TermLabel> |
ExpressionBuilder.visitLabel(KeYParser.LabelContext ctx) |
Modifier and Type | Method and Description |
---|---|
protected ImmutableArray<TermLabel> |
LogicPrinter.getVisibleTermLabels(Term t)
Determine the Set of labels that will be printed out for a specific
Term . |
protected ImmutableArray<TermLabel> |
SequentViewLogicPrinter.getVisibleTermLabels(Term t) |
Modifier and Type | Method and Description |
---|---|
boolean |
VisibleTermLabels.contains(TermLabel label) |
Modifier and Type | Method and Description |
---|---|
ImmutableArray<TermLabel> |
SVInstantiations.UpdateLabelPair.getUpdateApplicationlabels() |
Modifier and Type | Method and Description |
---|---|
SVInstantiations |
SVInstantiations.add(SchemaVariable sv,
ImmutableArray<TermLabel> labels,
Services services) |
SVInstantiations |
SVInstantiations.addUpdate(Term update,
ImmutableArray<TermLabel> updateApplicationlabels)
adds an update to the update context
|
Constructor and Description |
---|
UpdateLabelPair(Term update,
ImmutableArray<TermLabel> updateApplicationlabels) |
Modifier and Type | Method and Description |
---|---|
protected TermLabel |
FormulaTermLabelUpdate.getTermLabel(java.util.Set<TermLabel> labels,
Name name)
|
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)
|
Modifier and Type | Method and Description |
---|---|
boolean |
ChildTermLabelPolicy.addLabel(TermServices 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,
Term childTerm,
TermLabel label)
|
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)
|
boolean |
TermLabelMerger.mergeLabels(SequentFormula existingSF,
Term existingTerm,
TermLabel existingLabel,
SequentFormula rejectedSF,
Term rejectedTerm,
TermLabel rejectedLabel,
java.util.List<TermLabel> mergedLabels)
Merges the existing and the rejected
TermLabel by updating the merged List . |
boolean |
FormulaTermLabelMerger.mergeLabels(SequentFormula existingSF,
Term existingTerm,
TermLabel existingLabel,
SequentFormula rejectedSF,
Term rejectedTerm,
TermLabel rejectedLabel,
java.util.List<TermLabel> mergedLabels)
Merges the existing and the rejected
TermLabel by updating the merged List . |
Modifier and Type | Method and Description |
---|---|
protected TermLabel |
FormulaTermLabelUpdate.getTermLabel(java.util.Set<TermLabel> labels,
Name name)
|
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)
|
boolean |
TermLabelMerger.mergeLabels(SequentFormula existingSF,
Term existingTerm,
TermLabel existingLabel,
SequentFormula rejectedSF,
Term rejectedTerm,
TermLabel rejectedLabel,
java.util.List<TermLabel> mergedLabels)
Merges the existing and the rejected
TermLabel by updating the merged List . |
boolean |
FormulaTermLabelMerger.mergeLabels(SequentFormula existingSF,
Term existingTerm,
TermLabel existingLabel,
SequentFormula rejectedSF,
Term rejectedTerm,
TermLabel rejectedLabel,
java.util.List<TermLabel> mergedLabels)
Merges the existing and the rejected
TermLabel by updating the merged List . |
protected void |
FormulaTermLabelRefactoring.refactorBewlowUpdates(PosInOccurrence applicationPosInOccurrence,
Term term,
java.util.List<TermLabel> labels)
Refactors the
Term below its update. |
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. |
protected void |
FormulaTermLabelRefactoring.refactorSpecificationApplication(Term term,
Goal goal,
Services services,
java.util.List<TermLabel> labels,
java.lang.Object hint)
Refactors a specification application.
|
protected void |
FormulaTermLabelRefactoring.refactorSubstitution(Term term,
Term tacletTerm,
java.util.List<TermLabel> labels)
Refactors the given
Term after a substitiution. |
static FormulaTermLabel |
StayOnFormulaTermLabelPolicy.searchFormulaTermLabel(ImmutableArray<TermLabel> labels)
Searches the
FormulaTermLabel in the given TermLabel s. |
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 |
---|---|
static MatchInstruction |
Instruction.matchTermLabelSV(ImmutableArray<TermLabel> labels) |
Constructor and Description |
---|
MatchTermLabelInstruction(ImmutableArray<TermLabel> labels) |
Modifier and Type | Field and Description |
---|---|
static TermLabel |
DefinedSymbolsHandler.TRIGGER_LABEL |
Modifier and Type | Field and Description |
---|---|
ImmutableArray<TermLabel> |
PositionedLabeledString.labels |
Modifier and Type | Method and Description |
---|---|
ImmutableArray<TermLabel> |
PositionedString.getLabels()
returns list of labels attached to this positioned string
|
ImmutableArray<TermLabel> |
PositionedLabeledString.getLabels()
returns the labels attached to this positioned string
|
Modifier and Type | Method and Description |
---|---|
boolean |
PositionedString.containsLabel(TermLabel label)
checks if the given label is attached to the positioned string
|
boolean |
PositionedLabeledString.containsLabel(TermLabel label)
returns true if the given label is attached
|
PositionedLabeledString |
PositionedString.label(TermLabel label) |
Modifier and Type | Method and Description |
---|---|
PositionedLabeledString |
PositionedString.label(ImmutableArray<TermLabel> labels) |
Constructor and Description |
---|
PositionedLabeledString(java.lang.String text,
java.lang.String fileName,
Position pos,
TermLabel label) |
PositionedLabeledString(java.lang.String text,
java.lang.String fileName,
TermLabel label) |
PositionedLabeledString(java.lang.String text,
TermLabel label) |
Constructor and Description |
---|
PositionedLabeledString(java.lang.String text,
ImmutableArray<TermLabel> labels) |
PositionedLabeledString(java.lang.String text,
java.lang.String fileName,
ImmutableArray<TermLabel> labels) |
PositionedLabeledString(java.lang.String text,
java.lang.String fileName,
Position pos,
ImmutableArray<TermLabel> labels) |
Modifier and Type | Field and Description |
---|---|
TermLabel |
LabeledParserRuleContext.second |
Constructor and Description |
---|
LabeledParserRuleContext(org.antlr.v4.runtime.ParserRuleContext first,
TermLabel second) |
Modifier and Type | Method and Description |
---|---|
static TermFeature |
TermLabelTermFeature.create(TermLabel label) |
Constructor and Description |
---|
ContainsLabelFeature(TermLabel label) |
Modifier and Type | Field and Description |
---|---|
static TermLabel |
SymbolicExecutionUtil.LOOP_BODY_LABEL
Label attached to the modality which executes a loop body in branch
"Body Preserves Invariant" of applied "Loop Invariant" rules.
|
static TermLabel |
SymbolicExecutionUtil.LOOP_INVARIANT_NORMAL_BEHAVIOR_LABEL
Label attached to the implication when a loop body execution terminated
normally without any exceptions, returns or breaks in branch
"Body Preserves Invariant" of applied "Loop Invariant" rules to show the
loop invariant.
|
static TermLabel |
SymbolicExecutionUtil.RESULT_LABEL
Label attached to a
Term to evaluate in a side proof. |
Modifier and Type | Method and Description |
---|---|
static java.util.List<Pair<Term,Node>> |
SymbolicExecutionSideProofUtil.computeResults(Services services,
Proof proof,
ProofEnvironment sideProofEnvironment,
Sequent sequentToProve,
TermLabel label,
java.lang.String description,
java.lang.String methodTreatment,
java.lang.String loopTreatment,
java.lang.String queryTreatment,
java.lang.String splittingOption,
boolean addNamesToServices)
Starts the side proof and extracts the result
Term . |
static Term |
SymbolicExecutionUtil.removeLabelRecursive(TermFactory tf,
Term term,
TermLabel label)
|
Copyright © 2003-2019 The KeY-Project.