Package | Description |
---|---|
de.uka.ilkd.key.ldt |
This package contains the "language data types" (LDTs) of KeY.
|
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.rule.inst |
contains classes for the instantiation of schema variables of
Taclet s. |
de.uka.ilkd.key.rule.match.vm.instructions |
Modifier and Type | Method and Description |
---|---|
protected SortDependingFunction |
LDT.addSortDependingFunction(TermServices services,
java.lang.String kind) |
SortDependingFunction |
HeapLDT.getSelect(Sort instanceSort,
TermServices services)
Returns the select function for the given sort.
|
SortDependingFunction |
SeqLDT.getSeqGet(Sort instanceSort,
TermServices services) |
Modifier and Type | Method and Description |
---|---|
static SortDependingFunction |
SortDependingFunction.createFirstInstance(GenericSort sortDependingOn,
Name kind,
Sort sort,
Sort[] argSorts,
boolean unique) |
static SortDependingFunction |
SortDependingFunction.getFirstInstance(Name kind,
TermServices services) |
SortDependingFunction |
SortDependingFunction.getInstanceFor(Sort sort,
TermServices services)
returns the variant for the given sort
|
Modifier and Type | Method and Description |
---|---|
boolean |
SortDependingFunction.isSimilar(SortDependingFunction p) |
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 GenericSortCondition |
GenericSortCondition.createCondition(SortDependingFunction p0,
SortDependingFunction p1)
Create a condition ensuring that the two given symbols become
identical; "p0" may be of generic sort, "p1" not
|
Modifier and Type | Method and Description |
---|---|
static Instruction<SortDependingFunction> |
Instruction.matchSortDependingFunction(SortDependingFunction op) |
Modifier and Type | Method and Description |
---|---|
static Instruction<SortDependingFunction> |
Instruction.matchSortDependingFunction(SortDependingFunction op) |
Constructor and Description |
---|
MatchSortDependingFunctionInstruction(SortDependingFunction op) |
Copyright © 2003-2019 The KeY-Project.