Package | Description |
---|---|
de.uka.ilkd.key.logic |
provides a representation for the term and sequent
structure.
|
de.uka.ilkd.key.rule |
This package contains classes for implementing rules.
|
de.uka.ilkd.key.speclang.njml |
This package provides the functionalities of parsing JML comments into KeY constructs.
|
de.uka.ilkd.key.speclang.translation | |
de.uka.ilkd.key.taclettranslation.assumptions | |
de.uka.ilkd.key.util.mergerule |
Modifier and Type | Method and Description |
---|---|
Term |
TermBuilder.var(LogicVariable v) |
Modifier and Type | Method and Description |
---|---|
Pair<Term,Term> |
QueryExpand.queryEvalTerm(Services services,
Term query,
LogicVariable[] instVars)
Creates an invocation of a query in a modal operator and stores the value in a
new symbol.
|
Modifier and Type | Method and Description |
---|---|
Term |
JmlTermFactory.signals(Term result,
LogicVariable eVar,
ProgramVariable excVar,
KeYJavaType excType) |
Term |
JmlTermFactory.upperBound(Term a,
LogicVariable lv)
Extracts upper bound from
a if it matches the pattern. |
Modifier and Type | Method and Description |
---|---|
SLExpression |
JmlTermFactory.bsum(SLExpression a,
SLExpression b,
SLExpression t,
KeYJavaType declsType,
ImmutableList<LogicVariable> declVars) |
SLExpression |
JmlTermFactory.createUnionF(boolean nullable,
Pair<KeYJavaType,ImmutableList<LogicVariable>> declVars,
Term expr,
Term guard) |
SLExpression |
JmlTermFactory.exists(Term preTerm,
Term bodyTerm,
KeYJavaType declsType,
ImmutableList<LogicVariable> declVars,
boolean nullable,
KeYJavaType resultType) |
SLExpression |
JmlTermFactory.forall(Term preTerm,
Term bodyTerm,
KeYJavaType declsType,
ImmutableList<LogicVariable> declVars,
boolean nullable,
KeYJavaType resultType) |
SLExpression |
JmlTermFactory.quantifiedMax(Term _guard,
Term body,
KeYJavaType declsType,
boolean nullable,
ImmutableList<LogicVariable> qvs) |
SLExpression |
JmlTermFactory.quantifiedMin(Term _guard,
Term body,
KeYJavaType declsType,
boolean nullable,
ImmutableList<LogicVariable> qvs) |
SLExpression |
JmlTermFactory.quantifiedNumOf(Term t1,
Term t2,
KeYJavaType declsType,
boolean nullable,
java.lang.Iterable<LogicVariable> qvs,
KeYJavaType resultType) |
SLExpression |
JmlTermFactory.quantifiedProduct(KeYJavaType declsType,
boolean nullable,
java.lang.Iterable<LogicVariable> qvs,
Term t1,
Term t2,
KeYJavaType resultType) |
SLExpression |
JmlTermFactory.quantifiedSum(KeYJavaType javaType,
boolean nullable,
java.lang.Iterable<LogicVariable> qvs,
Term t1,
Term t2,
KeYJavaType resultType) |
Modifier and Type | Method and Description |
---|---|
void |
SLResolverManager.putIntoTopLocalVariablesNamespace(ImmutableList<LogicVariable> pvs,
KeYJavaType kjt)
Puts a list of local variables into the topmost namespace on the stack.
|
Modifier and Type | Field and Description |
---|---|
protected java.util.HashMap<java.lang.String,LogicVariable> |
AssumptionGenerator.usedVariables |
Modifier and Type | Method and Description |
---|---|
LogicVariable |
AssumptionGenerator.getInstantiationOfLogicVar(Sort instantiation,
LogicVariable lv) |
LogicVariable |
AssumptionGenerator.getLogicVariable(Name name,
Sort sort)
Returns a new logic variable with the given name and sort.
|
Modifier and Type | Method and Description |
---|---|
LogicVariable |
AssumptionGenerator.getInstantiationOfLogicVar(Sort instantiation,
LogicVariable lv) |
Modifier and Type | Method and Description |
---|---|
static LogicVariable |
MergeRuleUtils.getFreshVariableForPrefix(java.lang.String prefix,
Sort sort,
Services services)
Computes and registers a fresh variable with the given prefix in its name
of the given sort.
|
Modifier and Type | Method and Description |
---|---|
static Term |
MergeRuleUtils.substConstantsByFreshVars(Term term,
java.util.HashMap<Function,LogicVariable> replMap,
Services services)
Substitutes all constants in the given term by fresh variables.
|
static Term |
MergeRuleUtils.substConstantsByFreshVars(Term term,
java.util.HashSet<Function> restrictTo,
java.util.HashMap<Function,LogicVariable> replMap,
Services services)
Substitutes all constants in the given term that are contained in the set
restrictTo by fresh variables.
|
Copyright © 2003-2019 The KeY-Project.