Package | Description |
---|---|
de.uka.ilkd.key.java |
This package contains classes that cover the Java programming language.
|
de.uka.ilkd.key.ldt |
This package contains the "language data types" (LDTs) of KeY.
|
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.logic.sort |
This package contains different kinds and implementations subtyping interface Sort.
|
de.uka.ilkd.key.logic.util | |
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.proof.mgt |
This package contains classes for proof environments and proof management.
|
de.uka.ilkd.key.rule |
This package contains classes for implementing rules.
|
de.uka.ilkd.key.rule.conditions | |
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.merge | |
de.uka.ilkd.key.rule.metaconstruct |
contains classes representing the meta constructs of
Taclet s. |
de.uka.ilkd.key.rule.tacletbuilder | |
de.uka.ilkd.key.smt |
This package contains the SMT backend of KeY, allowing to translate KeY formulas
to formulas in formats such as SMT-LIB, and allowing to send such formulas to
SMT solvers such as Simplify or Z3.
|
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.quantifierHeuristics | |
de.uka.ilkd.key.strategy.termgenerator | |
de.uka.ilkd.key.symbolic_execution.rule | |
de.uka.ilkd.key.taclettranslation | |
de.uka.ilkd.key.taclettranslation.assumptions | |
de.uka.ilkd.key.taclettranslation.lemma |
Modifier and Type | Class and Description |
---|---|
class |
Services
this is a collection of common services to the KeY prover.
|
Modifier and Type | Method and Description |
---|---|
protected Function |
LDT.addFunction(TermServices services,
java.lang.String funcName)
looks up a function in the namespace and adds it to the LDT
|
protected SortDependingFunction |
LDT.addSortDependingFunction(TermServices services,
java.lang.String kind) |
Function |
HeapLDT.getClassErroneous(Sort instanceSort,
TermServices services) |
Function |
HeapLDT.getClassInitializationInProgress(Sort instanceSort,
TermServices services) |
Function |
HeapLDT.getClassInitialized(Sort instanceSort,
TermServices services) |
Function |
HeapLDT.getClassPrepared(Sort instanceSort,
TermServices services) |
SortDependingFunction |
HeapLDT.getSelect(Sort instanceSort,
TermServices services)
Returns the select function for the given sort.
|
SortDependingFunction |
SeqLDT.getSeqGet(Sort instanceSort,
TermServices services) |
boolean |
DoubleLDT.isResponsible(Operator op,
Term sub,
TermServices services,
ExecutionContext ec) |
boolean |
CharListLDT.isResponsible(Operator op,
Term sub,
TermServices services,
ExecutionContext ec) |
boolean |
FreeLDT.isResponsible(Operator op,
Term sub,
TermServices services,
ExecutionContext ec) |
boolean |
MapLDT.isResponsible(Operator op,
Term sub,
TermServices services,
ExecutionContext ec) |
boolean |
RealLDT.isResponsible(Operator op,
Term sub,
TermServices services,
ExecutionContext ec) |
boolean |
BooleanLDT.isResponsible(Operator op,
Term sub,
TermServices services,
ExecutionContext ec) |
boolean |
PermissionLDT.isResponsible(Operator op,
Term sub,
TermServices services,
ExecutionContext ec) |
boolean |
LocSetLDT.isResponsible(Operator op,
Term sub,
TermServices services,
ExecutionContext ec) |
boolean |
IntegerLDT.isResponsible(Operator op,
Term sub,
TermServices services,
ExecutionContext ec) |
boolean |
HeapLDT.isResponsible(Operator op,
Term sub,
TermServices services,
ExecutionContext ec) |
boolean |
FloatLDT.isResponsible(Operator op,
Term sub,
TermServices services,
ExecutionContext ec) |
boolean |
SeqLDT.isResponsible(Operator op,
Term sub,
TermServices services,
ExecutionContext ec) |
abstract boolean |
LDT.isResponsible(Operator op,
Term sub,
TermServices services,
ExecutionContext ec)
returns true if the LDT offers an operation for the given
unary java operator and the logic subterms
|
Constructor and Description |
---|
BooleanLDT(TermServices services) |
CharListLDT(TermServices services) |
DoubleLDT(TermServices services) |
FloatLDT(TermServices services) |
FreeLDT(TermServices services) |
HeapLDT(TermServices services) |
LDT(Name name,
Sort targetSort,
TermServices services) |
LDT(Name name,
TermServices services) |
LocSetLDT(TermServices services) |
MapLDT(TermServices services) |
RealLDT(TermServices services) |
SeqLDT(TermServices services) |
Modifier and Type | Method and Description |
---|---|
boolean |
BoundVariableTools.equalsModRenaming(ImmutableArray<QuantifiableVariable> vars0,
Term term0,
ImmutableArray<QuantifiableVariable> vars1,
Term term1,
TermServices services) |
Term |
TermBuilder.fieldStore(TermServices services,
Term o,
Function f,
Term v) |
Term |
TermBuilder.max(ImmutableList<? extends QuantifiableVariable> qvs,
Term range,
Term t,
TermServices services)
minimum operator
|
Term |
TermBuilder.min(ImmutableList<? extends QuantifiableVariable> qvs,
Term range,
Term t,
TermServices services)
minimum operator
|
Term |
TermBuilder.prod(ImmutableList<QuantifiableVariable> qvs,
Term range,
Term t,
TermServices services)
General (unbounded) product
|
Term[] |
BoundVariableTools.renameVariables(Term[] originalTerms,
ImmutableArray<QuantifiableVariable> oldBoundVars,
ImmutableArray<QuantifiableVariable> newBoundVars,
TermServices services) |
Term |
BoundVariableTools.renameVariables(Term originalTerm,
ImmutableArray<QuantifiableVariable> oldBoundVars,
ImmutableArray<QuantifiableVariable> newBoundVars,
TermServices services)
Compare the arrays
oldBoundVars and
newBoundVars component-wise, and in case of differences
substitute variables from the former array with the ones of the latter
array (in originalTerm ) |
boolean |
BoundVariableTools.resolveCollisions(Term originalTerm,
ImmutableSet<QuantifiableVariable> criticalVars,
ImmutableArray<QuantifiableVariable>[] newBoundVars,
Term[] newSubs,
TermServices services)
Ensure that none of the variables
criticalVars is bound by
the top-level operator of t (by bound renaming). |
ImmutableArray<QuantifiableVariable> |
BoundVariableTools.unifyBoundVariables(ImmutableArray<QuantifiableVariable>[] boundVarsPerSub,
Term[] subs,
int subtermsBegin,
int subtermsEnd,
TermServices services)
Ensure that for the subterms with indexes [
subtermsBegin ,
subtermsEnd ) the same variables are bound. |
Modifier and Type | Method and Description |
---|---|
protected java.util.Map<Name,ChildTermLabelPolicy> |
TermLabelManager.computeActiveChildPolicies(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,java.util.Map<Name,ChildTermLabelPolicy>> ruleSpecificPolicies,
java.util.Map<Name,ChildTermLabelPolicy> ruleIndependentPolicies)
Computes active
ChildTermLabelPolicy instances which have to be executed during the given rule application. |
T |
SingletonLabelFactory.parseInstance(java.util.List<java.lang.String> arguments,
TermServices services)
Parses the arguments and produces a term label.
|
OriginTermLabel |
OriginTermLabelFactory.parseInstance(java.util.List<java.lang.String> arguments,
TermServices services) |
BlockContractValidityTermLabel |
BlockContractValidityTermLabelFactory.parseInstance(java.util.List<java.lang.String> parameters,
TermServices services)
Parses the arguments and produces a term label.
|
FormulaTermLabel |
FormulaTermLabelFactory.parseInstance(java.util.List<java.lang.String> parameters,
TermServices services)
Parses the arguments and produces a term label.
|
T |
TermLabelFactory.parseInstance(java.util.List<java.lang.String> arguments,
TermServices services)
Parses the arguments and produces a term label.
|
SymbolicExecutionTermLabel |
SymbolicExecutionTermLabelFactory.parseInstance(java.util.List<java.lang.String> parameters,
TermServices services)
Parses the arguments and produces a term label.
|
TermLabel |
TermLabelManager.parseLabel(java.lang.String name,
java.util.List<java.lang.String> args,
TermServices services)
Get a term label for string parameters.
|
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. |
Modifier and Type | Method and Description |
---|---|
static SortDependingFunction |
SortDependingFunction.getFirstInstance(Name kind,
TermServices services) |
SortDependingFunction |
SortDependingFunction.getInstanceFor(Sort sort,
TermServices services)
returns the variant for the given sort
|
static Transformer |
Transformer.getTransformer(Name name,
Sort sort,
ImmutableArray<Sort> argSorts,
TermServices services)
Looks up the function namespace for a term transformer with the given
attributes, assuming it to be uniquely defined by its name.
|
static Transformer |
Transformer.getTransformer(Transformer t,
TermServices services)
Takes a template for a term transformer and checks in the function
namespace, whether an equivalent already exists.
|
Modifier and Type | Method and Description |
---|---|
SortDependingFunction |
NullSort.getCastSymbol(TermServices services) |
SortDependingFunction |
AbstractSort.getCastSymbol(TermServices services) |
SortDependingFunction |
Sort.getCastSymbol(TermServices services) |
SortDependingFunction |
NullSort.getExactInstanceofSymbol(TermServices services) |
SortDependingFunction |
AbstractSort.getExactInstanceofSymbol(TermServices services) |
SortDependingFunction |
Sort.getExactInstanceofSymbol(TermServices services) |
SortDependingFunction |
NullSort.getInstanceofSymbol(TermServices services) |
SortDependingFunction |
AbstractSort.getInstanceofSymbol(TermServices services) |
SortDependingFunction |
Sort.getInstanceofSymbol(TermServices services) |
Modifier and Type | Method and Description |
---|---|
static Sort |
TermHelper.getMaxSort(Term term,
int i,
TermServices services)
helper function to determine the maximal sort the term
tSub may have as i sub term
This method will become obsolete in the near future as all operators
will become a fixed signature.
|
Modifier and Type | Method and Description |
---|---|
ImmutableList<NoPosTacletApp> |
TacletAppIndex.getFindTaclet(PosInOccurrence pos,
TacletFilter filter,
TermServices services)
collects all FindTaclets with instantiations and position
|
ImmutableList<NoPosTacletApp> |
RuleAppIndex.getFindTaclet(TacletFilter filter,
PosInOccurrence pos,
TermServices services)
collects all FindTacletInstantiations for the given
heuristics and position
|
ImmutableList<NoPosTacletApp> |
TacletAppIndex.getRewriteTaclet(PosInOccurrence pos,
TacletFilter filter,
TermServices services)
collects all RewriteTacletInstantiations in a subterm of the
constrainedFormula described by a PosInOccurrence.
|
ImmutableList<NoPosTacletApp> |
RuleAppIndex.getRewriteTaclet(TacletFilter filter,
PosInOccurrence pos,
TermServices services)
collects all RewriteTacletInstantiations for the given
heuristics in a subterm of the constraintformula described by a
PosInOccurrence
|
Modifier and Type | Method and Description |
---|---|
RuleJustification |
RuleJustificationInfo.getJustification(RuleApp r,
TermServices services) |
RuleJustification |
ComplexRuleJustification.getSpecificJustification(RuleApp app,
TermServices services) |
RuleJustification |
ComplexRuleJustificationBySpec.getSpecificJustification(RuleApp app,
TermServices services) |
Modifier and Type | Method and Description |
---|---|
static java.util.Map<LocationVariable,LocationVariable> |
UseOperationContractRule.computeAtPreVars(java.util.List<LocationVariable> heapContext,
TermServices services,
UseOperationContractRule.Instantiation inst)
Returns the correct pre-heap variables.
|
static ProgramVariable |
UseOperationContractRule.computeResultVar(UseOperationContractRule.Instantiation inst,
TermServices services)
Computes the result variable for this instantiation.
|
protected static java.util.Map<LocationVariable,Function> |
AbstractBlockContractRule.createAndRegisterAnonymisationVariables(java.lang.Iterable<LocationVariable> variables,
BlockContract contract,
TermServices services) |
protected java.util.Map<LocationVariable,Function> |
AbstractLoopContractRule.createAndRegisterAnonymisationVariables(java.lang.Iterable<LocationVariable> variables,
LoopContract contract,
TermServices services) |
IBuiltInRuleApp |
BlockContractExternalRule.createApp(PosInOccurrence pos,
TermServices services) |
DefaultBuiltInRuleApp |
QueryExpand.createApp(PosInOccurrence pos,
TermServices services) |
OneStepSimplifierRuleApp |
OneStepSimplifier.createApp(PosInOccurrence pos,
TermServices services) |
LoopInvariantBuiltInRuleApp |
WhileInvariantRule.createApp(PosInOccurrence pos,
TermServices services) |
BlockContractInternalBuiltInRuleApp |
BlockContractInternalRule.createApp(PosInOccurrence occurrence,
TermServices services) |
IBuiltInRuleApp |
LoopContractExternalRule.createApp(PosInOccurrence pos,
TermServices services) |
IBuiltInRuleApp |
BuiltInRule.createApp(PosInOccurrence pos,
TermServices services) |
LoopContractInternalBuiltInRuleApp |
LoopContractInternalRule.createApp(PosInOccurrence occurrence,
TermServices services) |
UseDependencyContractApp |
UseDependencyContractRule.createApp(PosInOccurrence pos,
TermServices services) |
IBuiltInRuleApp |
LoopApplyHeadRule.createApp(PosInOccurrence pos,
TermServices services) |
ContractRuleApp |
UseOperationContractRule.createApp(PosInOccurrence pos,
TermServices services) |
IBuiltInRuleApp |
AbstractLoopInvariantRule.createApp(PosInOccurrence pos,
TermServices services) |
static PosInOccurrence |
UseDependencyContractRule.findStepInIfInsts(java.util.List<PosInOccurrence> steps,
UseDependencyContractApp app,
TermServices services) |
Sort |
TacletApp.getRealSort(SchemaVariable p_sv,
TermServices services) |
boolean |
TacletApp.isExecutable(TermServices services) |
protected static Pair<Term,Term> |
AbstractLoopInvariantRule.prepareVariant(AbstractLoopInvariantRule.Instantiation inst,
Term variant,
TermServices services)
Creates the variant proof obligation and update.
|
protected Term |
QueryExpand.replace(Term term,
Term with,
java.util.Iterator<java.lang.Integer> it,
TermServices services)
Replaces in a term.
|
protected MatchConditions |
NoPosTacletApp.setupMatchConditions(PosInOccurrence pos,
TermServices services) |
protected static Pair<Term,Term> |
AbstractLoopInvariantRule.splitUpdates(Term focusTerm,
TermServices services)
Splits a term into the update and formula part.
|
PosInOccurrence |
UseDependencyContractApp.step(Sequent seq,
TermServices services) |
Constructor and Description |
---|
LoopInvariantBuiltInRuleApp(BuiltInRule rule,
PosInOccurrence pio,
ImmutableList<PosInOccurrence> ifInsts,
LoopSpecification inv,
java.util.List<LocationVariable> heapContext,
TermServices services) |
LoopInvariantBuiltInRuleApp(BuiltInRule rule,
PosInOccurrence pio,
LoopSpecification inv,
TermServices services) |
LoopInvariantBuiltInRuleApp(BuiltInRule rule,
PosInOccurrence pos,
TermServices services) |
Modifier and Type | Method and Description |
---|---|
abstract boolean |
TypeResolver.isComplete(SchemaVariable sv,
SVSubstitute instCandidate,
SVInstantiations instMap,
TermServices services) |
boolean |
TypeResolver.GenericSortResolver.isComplete(SchemaVariable sv,
SVSubstitute instCandidate,
SVInstantiations instMap,
TermServices services) |
boolean |
TypeResolver.NonGenericSortResolver.isComplete(SchemaVariable sv,
SVSubstitute instCandidate,
SVInstantiations instMap,
TermServices services) |
boolean |
TypeResolver.ElementTypeResolverForSV.isComplete(SchemaVariable sv,
SVSubstitute instCandidate,
SVInstantiations instMap,
TermServices services) |
boolean |
TypeResolver.ContainerTypeResolver.isComplete(SchemaVariable sv,
SVSubstitute instCandidate,
SVInstantiations instMap,
TermServices services) |
Modifier and Type | Method and Description |
---|---|
Sort |
GenericSortInstantiations.getRealSort(SchemaVariable p_sv,
TermServices services) |
Sort |
GenericSortInstantiations.getRealSort(Sort p_s,
TermServices services) |
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)
|
boolean |
ChildTermLabelPolicy.isRuleApplicationSupported(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)
Decides if the currently active
Rule application is supported or not. |
Modifier and Type | Method and Description |
---|---|
IBuiltInRuleApp |
MergeRule.createApp(PosInOccurrence pio,
TermServices services) |
IBuiltInRuleApp |
CloseAfterMerge.createApp(PosInOccurrence pos,
TermServices services) |
Modifier and Type | Method and Description |
---|---|
KeYJavaType |
ProgramTransformer.getKeYJavaType(TermServices javaServ) |
Modifier and Type | Method and Description |
---|---|
Taclet |
TacletGenerator.generateAxiomTaclet(Name tacletName,
Term originalAxiom,
ImmutableList<ProgramVariable> programVars,
KeYJavaType kjt,
RuleSet ruleSet,
TermServices services)
Returns a no-find taclet to the passed axiom.
|
ImmutableSet<Taclet> |
TacletGenerator.generateContractAxiomTaclets(Name name,
Term originalPre,
Term originalPost,
Term originalMby,
KeYJavaType kjt,
IObserverFunction target,
java.util.List<? extends ProgramVariable> heaps,
ProgramVariable originalSelfVar,
ProgramVariable originalResultVar,
java.util.Map<LocationVariable,ProgramVariable> atPreVars,
ImmutableList<ProgramVariable> originalParamVars,
ImmutableSet<Pair<Sort,IObserverFunction>> toLimit,
boolean satisfiabilityGuard,
TermServices services) |
Taclet |
TacletGenerator.generateRelationalRepresentsTaclet(Name tacletName,
Term originalAxiom,
KeYJavaType kjt,
IObserverFunction target,
java.util.List<? extends ProgramVariable> heaps,
ProgramVariable self,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,ProgramVariable> atPreVars,
boolean satisfiabilityGuard,
TermServices services) |
Taclet |
TacletGenerator.generateRewriteTaclet(Name tacletName,
Term originalFind,
Term originalAxiom,
ImmutableList<ProgramVariable> programVars,
RuleSet ruleSet,
TermServices services) |
Modifier and Type | Method and Description |
---|---|
TermServices |
ProblemTypeInformation.getServices() |
Modifier and Type | Method and Description |
---|---|
RuleAppSMT |
RuleAppSMT.SMTRule.createApp(PosInOccurrence pos,
TermServices services) |
Constructor and Description |
---|
ProblemTypeInformation(TermServices services) |
Modifier and Type | Method and Description |
---|---|
MethodWellDefinedness |
MethodWellDefinedness.combine(WellDefinednessCheck wdc,
TermServices services) |
ClassWellDefinedness |
ClassWellDefinedness.combine(WellDefinednessCheck wdc,
TermServices services) |
WellDefinednessCheck |
WellDefinednessCheck.combine(WellDefinednessCheck wdc,
TermServices services)
Combines two well-definedness checks having the same name, id, target, type,
behaviour and are either both model fields or both not a model field.
|
LoopWellDefinedness |
LoopWellDefinedness.combine(WellDefinednessCheck wdc,
TermServices services) |
BlockWellDefinedness |
BlockWellDefinedness.combine(WellDefinednessCheck wdc,
TermServices services) |
RewriteTaclet |
MethodWellDefinedness.combineTaclets(RewriteTaclet t1,
RewriteTaclet t2,
TermServices services)
Combines two well-definedness taclets for (pure) method invocations.
|
static java.util.Map<LocationVariable,LocationVariable> |
HeapContext.getBeforeAtPreVars(java.util.List<LocationVariable> heaps,
TermServices services,
java.lang.String contextName) |
Term |
InitiallyClauseImpl.getClause(ParsableVariable selfVar,
TermServices services) |
Term |
InitiallyClause.getClause(ParsableVariable selfVar,
TermServices services)
Returns the formula without implicit all-quantification over
the receiver object.
|
Term |
AbstractAuxiliaryContractImpl.getInstantiationSelfTerm(TermServices services) |
Term |
AuxiliaryContract.getInstantiationSelfTerm(TermServices services) |
Term |
ClassInvariantImpl.getInv(ParsableVariable selfVar,
TermServices services) |
Term |
ClassInvariant.getInv(ParsableVariable selfVar,
TermServices services)
Returns the invariant formula without implicit all-quantification over
the receiver object.
|
Term |
WellDefinednessCheck.getPost(de.uka.ilkd.key.speclang.WellDefinednessCheck.Condition post,
ParsableVariable result,
TermServices services)
Gets the full valid post-condition
|
Term |
WellDefinednessCheck.getUpdates(Term mod,
LocationVariable heap,
ProgramVariable heapAtPre,
Term anonHeap,
TermServices services)
Gets the necessary updates applicable to the post-condition
|
boolean |
MethodWellDefinedness.isNormal(TermServices services)
Used to determine if the contract of this method has normal behaviour or
is a model field/method and can thus not throw any exception.
|
Constructor and Description |
---|
Variables(ProgramVariable self,
java.util.Map<Label,ProgramVariable> breakFlags,
java.util.Map<Label,ProgramVariable> continueFlags,
ProgramVariable returnFlag,
ProgramVariable result,
ProgramVariable exception,
java.util.Map<LocationVariable,LocationVariable> remembranceHeaps,
java.util.Map<LocationVariable,LocationVariable> remembranceLocalVariables,
java.util.Map<LocationVariable,LocationVariable> outerRemembranceHeaps,
java.util.Map<LocationVariable,LocationVariable> outerRemembranceVariables,
TermServices services)
You should use
#create() instead of this constructor. |
Modifier and Type | Method and Description |
---|---|
SLExpression |
JmlTermFactory.skolemExprHelper(KeYJavaType type,
TermServices services,
java.lang.String shortName) |
SLExpression |
JmlTermFactory.skolemExprHelper(java.lang.String jmlKeyWord,
KeYJavaType type,
TermServices services) |
SLExpression |
JmlTermFactory.skolemExprHelper(org.antlr.runtime.Token jmlKeyWord,
KeYJavaType type,
TermServices services) |
Modifier and Type | Method and Description |
---|---|
Term |
Substitution.apply(Term t,
TermServices services) |
Term |
Substitution.applyWithoutCasts(Term t,
TermServices services)
Try to apply the substitution to a term, introducing casts if
necessary (may never be the case any more, XXX)
|
Constraint |
Constraint.join(Constraint co,
TermServices services)
Deprecated.
joins the given constraint with this constraint and returns the joint new
constraint.
|
Constraint |
Constraint.Top.join(Constraint co,
TermServices services)
Deprecated.
joint of Top and co is Top
|
Constraint |
EqualityConstraint.join(Constraint co,
TermServices services)
Deprecated.
joins the given constraint with this constraint
and returns the joint new constraint.
|
Constraint |
Constraint.join(Constraint co,
TermServices services,
BooleanContainer unchanged)
Deprecated.
joins constraint co with this constraint and returns the joint new
constraint.
|
Constraint |
Constraint.Top.join(Constraint co,
TermServices services,
BooleanContainer c)
Deprecated.
joint of Top and co is Top and Top subsumes every constraint
|
Constraint |
EqualityConstraint.join(Constraint co,
TermServices services,
BooleanContainer unchanged)
Deprecated.
joins constraint co with this constraint
and returns the joint new constraint.
|
Constraint |
Constraint.unify(Term t1,
Term t2,
TermServices services)
Deprecated.
tries to unify the terms t1 and t2
|
Constraint |
Constraint.Top.unify(Term t1,
Term t2,
TermServices services)
Deprecated.
adding new constraints to an unsatisfiable constraint results in an
unsatisfiable constraint so this one is returned
|
Constraint |
EqualityConstraint.unify(Term t1,
Term t2,
TermServices services)
Deprecated.
unifies terms t1 and t2
|
Constraint |
Constraint.unify(Term t1,
Term t2,
TermServices services,
BooleanContainer unchanged)
Deprecated.
tries to unify terms t1 and t2.
|
Constraint |
Constraint.Top.unify(Term t1,
Term t2,
TermServices services,
BooleanContainer unchanged)
Deprecated.
|
Constraint |
EqualityConstraint.unify(Term t1,
Term t2,
TermServices services,
BooleanContainer unchanged)
Deprecated.
executes unification for terms t1 and t2.
|
Modifier and Type | Method and Description |
---|---|
static TermGenerator |
RootsGenerator.create(ProjectionToTerm powerRelation,
TermServices services) |
Modifier and Type | Method and Description |
---|---|
IBuiltInRuleApp |
ModalitySideProofRule.createApp(PosInOccurrence pos,
TermServices services) |
IBuiltInRuleApp |
QuerySideProofRule.createApp(PosInOccurrence pos,
TermServices services) |
Modifier and Type | Method and Description |
---|---|
Term |
TacletFormula.getFormula(TermServices services) |
Term |
SkeletonGenerator.translate(Taclet t,
TermServices services)
Override this method to introduce a translating mechanism for taclets.
|
Term |
DefaultTacletTranslator.translate(Taclet taclet,
TermServices services)
Translates a RewriteTaclet to a formula.
|
Modifier and Type | Method and Description |
---|---|
Term |
AssumptionFormula.getFormula(TermServices services) |
protected static Term |
AssumptionGenerator.quantifyTerm(Term term,
TermServices services)
Quantifies a term, i.d.
|
Modifier and Type | Method and Description |
---|---|
protected Operator |
GenericRemovingLemmaGenerator.replaceOp(Operator op,
TermServices services)
Sometimes operators must be replaced during lemma generation.
|
protected Sort |
GenericRemovingLemmaGenerator.replaceSort(Sort sort,
TermServices services)
Sometimes sorts must be replaced during lemma generation.
|
TacletFormula |
LemmaGenerator.translate(Taclet taclet,
TermServices services) |
Copyright © 2003-2019 The KeY-Project.