Package | Description |
---|---|
de.uka.ilkd.key.java |
This package contains classes that cover the Java programming language.
|
de.uka.ilkd.key.logic |
provides a representation for the term and sequent
structure.
|
de.uka.ilkd.key.logic.label | |
de.uka.ilkd.key.nparser.builder | |
de.uka.ilkd.key.proof |
This package contains the core data structures of proofs, nodes, goals, as well
as machinery to deal with these data structures.
|
de.uka.ilkd.key.rule |
This package contains classes for implementing rules.
|
de.uka.ilkd.key.symbolic_execution.util |
Modifier and Type | Method and Description |
---|---|
TermFactory |
Services.getTermFactory()
Returns the
TermFactory used to create Term s. |
Modifier and Type | Method and Description |
---|---|
TermFactory |
TermServices.getTermFactory()
Returns the
TermBuilder used to create Term s. |
TermFactory |
TermBuilder.tf() |
Constructor and Description |
---|
TermBuilder(TermFactory tf,
Services services) |
Modifier and Type | Method and Description |
---|---|
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 Term |
TermLabel.removeIrrelevantLabels(Term term,
TermFactory tf)
Remove all irrelevant labels from a term.
|
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 | Method and Description |
---|---|
TermFactory |
ExpressionBuilder.getTermFactory() |
Modifier and Type | Method and Description |
---|---|
static <S extends SVSubstitute,T> |
ReplacementMap.create(TermFactory tf,
Proof proof)
Creates a new replacement map.
|
static <S extends SVSubstitute,T> |
ReplacementMap.create(TermFactory tf,
Proof proof,
java.util.Map<S,T> initialMappings)
Creates a new replacement map.
|
static Term |
OpReplacer.replace(Operator toReplace,
Operator with,
Term in,
TermFactory tf)
Replace an operator.
|
static Term |
OpReplacer.replace(Operator toReplace,
Operator with,
Term in,
TermFactory tf,
Proof proof)
Replace an operator.
|
static ImmutableList<Term> |
OpReplacer.replace(Term toReplace,
Term with,
ImmutableList<Term> in,
TermFactory tf)
Replace a sub-term.
|
static ImmutableList<Term> |
OpReplacer.replace(Term toReplace,
Term with,
ImmutableList<Term> in,
TermFactory tf,
Proof proof)
Replace a sub-term.
|
static Term |
OpReplacer.replace(Term toReplace,
Term with,
Term in,
TermFactory tf)
Replace a sub-term.
|
static Term |
OpReplacer.replace(Term toReplace,
Term with,
Term in,
TermFactory tf,
Proof proof)
Replace a sub-term.
|
Constructor and Description |
---|
NoIrrelevantLabelsReplacementMap(TermFactory tf)
Create a new map
|
OpReplacer(java.util.Map<? extends SVSubstitute,? extends SVSubstitute> map,
TermFactory tf)
Creates an
OpReplacer . |
OpReplacer(java.util.Map<? extends SVSubstitute,? extends SVSubstitute> map,
TermFactory tf,
Proof proof)
Creates an
OpReplacer . |
Modifier and Type | Method and Description |
---|---|
static ImmutableList<Term> |
UseOperationContractRule.computeParams(Term baseHeapTerm,
java.util.Map<LocationVariable,Term> atPres,
LocationVariable baseHeap,
UseOperationContractRule.Instantiation inst,
TermFactory tf)
Returns the correct parameter terms.
|
static Term |
UseOperationContractRule.computeSelf(Term baseHeapTerm,
java.util.Map<LocationVariable,Term> atPres,
LocationVariable baseHeap,
UseOperationContractRule.Instantiation inst,
Term resultTerm,
TermFactory tf)
Returns the correct self term.
|
Modifier and Type | Method and Description |
---|---|
protected static Sequent |
SymbolicExecutionUtil.labelSkolemConstants(Sequent sequent,
java.util.Set<Term> constantsToLabel,
TermFactory factory)
Labels all specified skolem equalities with the
SymbolicExecutionUtil.RESULT_LABEL . |
static Term |
SymbolicExecutionUtil.removeLabelRecursive(TermFactory tf,
Term term,
TermLabel label)
|
Copyright © 2003-2019 The KeY-Project.