Package | Description |
---|---|
de.uka.ilkd.key.axiom_abstraction.predicateabstraction | |
de.uka.ilkd.key.core | |
de.uka.ilkd.key.java |
This package contains classes that cover the Java programming language.
|
de.uka.ilkd.key.java.abstraction |
This package contains the meta model abstractions as used by the
semantical services.
|
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.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.macros.scripts |
Proof script commands are a simple proof automation facility.
|
de.uka.ilkd.key.nparser.builder | |
de.uka.ilkd.key.parser |
This package contains the parser for .key and .proof files.
|
de.uka.ilkd.key.pp |
This package contains pretty-printing functionality used by the GUI and for
saving proofs.
|
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.init |
This package contains classes handling prover initialisation.
|
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.merge.procedures | |
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.smt.hierarchy | |
de.uka.ilkd.key.smt.model | |
de.uka.ilkd.key.smt.newsmt2 | |
de.uka.ilkd.key.speclang |
This package contains the specification language frontends of KeY.
|
de.uka.ilkd.key.strategy |
This package contains classes implementing the proof search strategies of KeY.
|
de.uka.ilkd.key.strategy.feature | |
de.uka.ilkd.key.strategy.quantifierHeuristics | |
de.uka.ilkd.key.strategy.termfeature | |
de.uka.ilkd.key.symbolic_execution | |
de.uka.ilkd.key.symbolic_execution.model | |
de.uka.ilkd.key.symbolic_execution.model.impl | |
de.uka.ilkd.key.symbolic_execution.object_model | |
de.uka.ilkd.key.symbolic_execution.object_model.impl | |
de.uka.ilkd.key.symbolic_execution.rule | |
de.uka.ilkd.key.symbolic_execution.util | |
de.uka.ilkd.key.taclettranslation.assumptions | |
de.uka.ilkd.key.taclettranslation.lemma | |
de.uka.ilkd.key.testgen | |
de.uka.ilkd.key.testgen.oracle | |
de.uka.ilkd.key.util |
This package is a grab bag of miscellaneous useful code fragments.
|
de.uka.ilkd.key.util.mergerule |
Modifier and Type | Method and Description |
---|---|
Sort |
AbstractionPredicate.getArgSort() |
Modifier and Type | Method and Description |
---|---|
static AbstractionPredicate |
AbstractionPredicate.create(Sort argSort,
java.util.function.Function<Term,Term> mapping,
Services services)
Creates a new
AbstractionPredicate with the given name and
mapping. |
Modifier and Type | Method and Description |
---|---|
Namespace<Sort> |
KeYMediator.sort_ns()
returns the sort namespace
|
Modifier and Type | Method and Description |
---|---|
Sort |
JavaInfo.cloneableSort()
returns the KeYJavaType for class java.lang.Cloneable
|
Sort |
TypeConverter.getPrimitiveSort(Type t) |
Sort |
JavaInfo.nullSort() |
Sort |
JavaInfo.objectSort()
returns the KeYJavaType for class java.lang.Object
|
Sort |
JavaInfo.serializableSort()
returns the KeYJavaType for class java.io.Serializable
|
Modifier and Type | Method and Description |
---|---|
java.util.Map<Sort,java.util.Map<Sort,java.lang.Boolean>> |
ServiceCaches.getDisjointnessCache() |
java.util.Map<Sort,java.util.Map<Sort,java.lang.Boolean>> |
ServiceCaches.getDisjointnessCache() |
Modifier and Type | Method and Description |
---|---|
Term |
TypeConverter.findThisForSort(Sort s,
ExecutionContext ec) |
Term |
TypeConverter.findThisForSort(Sort s,
Term self,
KeYJavaType context,
boolean exact) |
Term |
TypeConverter.findThisForSortExact(Sort s,
ExecutionContext ec) |
ProgramVariable |
JavaInfo.getAttribute(java.lang.String attributeName,
Sort s)
returns an attribute named attributeName declared locally
in object type s
|
KeYJavaType |
JavaInfo.getKeYJavaType(Sort sort)
returns a KeYJavaType having the given sort
|
LDT |
TypeConverter.getModelFor(Sort s) |
boolean |
JavaInfo.isAJavaCommonSort(Sort sort)
tests if sort represents java.lang.Object, java.lang.Cloneable or
java.io.Serializable
|
java.util.List<KeYJavaType> |
JavaInfo.lookupSort2KJTCache(Sort sort) |
Constructor and Description |
---|
CreateArrayMethodBuilder(KeYJavaType integerType,
KeYJavaType objectType,
Sort heapSort,
int heapCount)
create the method builder for array implict creation methods
|
Modifier and Type | Method and Description |
---|---|
Sort |
KeYJavaType.getSort() |
Modifier and Type | Method and Description |
---|---|
void |
KeYJavaType.setSort(Sort s) |
Constructor and Description |
---|
KeYJavaType(Sort sort)
creates a new KeYJavaType
|
KeYJavaType(Type javaType,
Sort sort)
creates a new KeYJavaType
|
Modifier and Type | Method and Description |
---|---|
Sort |
HeapLDT.getFieldSort()
Returns the sort "Field".
|
Sort |
HeapLDT.getSortOfSelect(Operator op)
If the passed operator is an instance of "select", this method returns
the sort of the function (identical to its return type); otherwise,
returns null.
|
Sort |
LDT.targetSort()
Returns the sort associated with the LDT.
|
Modifier and Type | Method and Description |
---|---|
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) |
Constructor and Description |
---|
LDT(Name name,
Sort targetSort,
TermServices services) |
Modifier and Type | Method and Description |
---|---|
Sort |
TermImpl.sort() |
Sort |
Term.sort()
The sort of the term.
|
Sort |
Sorted.sort() |
Modifier and Type | Method and Description |
---|---|
java.util.Set<Sort> |
SortCollector.getSorts() |
ImmutableList<Sort> |
TermBuilder.getSorts(java.lang.Iterable<Term> terms)
|
Namespace<Sort> |
NamespaceSet.sorts() |
Modifier and Type | Method and Description |
---|---|
Term |
TermBuilder.cast(Sort s,
Term t) |
Term |
TermBuilder.classErroneous(Sort classSort) |
Term |
TermBuilder.classInitializationInProgress(Sort classSort) |
Term |
TermBuilder.classInitialized(Sort classSort) |
Term |
TermBuilder.classPrepared(Sort classSort) |
Term |
TermBuilder.dot(Sort asSort,
Term o,
Function f) |
Term |
TermBuilder.dot(Sort asSort,
Term o,
LocationVariable field) |
Term |
TermBuilder.dot(Sort asSort,
Term o,
Term f) |
Term |
TermBuilder.exactInstance(Sort s,
Term t) |
LocationVariable |
TermBuilder.heapAtPreVar(java.lang.String baseName,
Sort sort,
boolean makeNameUnique)
Creates a program variable for the atPre heap.
|
Term |
TermBuilder.instance(Sort s,
Term t) |
java.lang.String |
TermBuilder.newName(Sort sort)
Returns an available name constructed by affixing a counter to a self-
chosen base name for the passed sort.
|
Term |
TermBuilder.select(Sort asSort,
Term h,
Term o,
LocationVariable field)
Get the select expression for a location variabe representing the field.
|
Term |
TermBuilder.select(Sort asSort,
Term h,
Term o,
Term f) |
Term |
TermBuilder.seqGet(Sort asSort,
Term s,
Term idx) |
java.lang.String |
TermBuilder.shortBaseName(Sort s) |
Term |
TermBuilder.staticDot(Sort asSort,
Function f) |
Term |
TermBuilder.staticDot(Sort asSort,
Term f) |
Modifier and Type | Method and Description |
---|---|
void |
NamespaceSet.setSorts(Namespace<Sort> sortNS) |
Constructor and Description |
---|
NamespaceSet(Namespace<QuantifiableVariable> varNS,
Namespace<Function> funcNS,
Namespace<Sort> sortNS,
Namespace<RuleSet> ruleSetNS,
Namespace<Choice> choiceNS,
Namespace<IProgramVariable> programVarNS) |
Modifier and Type | Field and Description |
---|---|
static Sort |
AbstractTermTransformer.METASORT
The metasort sort
|
Modifier and Type | Method and Description |
---|---|
Sort |
SortedOperator.argSort(int i) |
Sort |
AbstractSortedOperator.argSort(int i) |
Sort |
SortDependingFunction.getSortDependingOn() |
Sort |
SortedOperator.sort() |
Sort |
AbstractSortedOperator.sort() |
Sort |
SubstOp.sort(ImmutableArray<Term> terms) |
Sort |
IfThenElse.sort(ImmutableArray<Term> terms) |
Sort |
AbstractSortedOperator.sort(ImmutableArray<Term> terms) |
Sort |
UpdateApplication.sort(ImmutableArray<Term> terms) |
Sort |
Operator.sort(ImmutableArray<Term> terms)
Determines the sort of the
Term if it would be created using this
Operator as top level operator and the given terms as sub terms. |
Sort |
IfExThenElse.sort(ImmutableArray<Term> terms) |
Modifier and Type | Method and Description |
---|---|
ImmutableArray<Sort> |
SortedOperator.argSorts() |
ImmutableArray<Sort> |
AbstractSortedOperator.argSorts() |
Modifier and Type | Method and Description |
---|---|
static SortDependingFunction |
SortDependingFunction.createFirstInstance(GenericSort sortDependingOn,
Name kind,
Sort sort,
Sort[] argSorts,
boolean unique) |
static SortDependingFunction |
SortDependingFunction.createFirstInstance(GenericSort sortDependingOn,
Name kind,
Sort sort,
Sort[] argSorts,
boolean unique) |
static ModalOperatorSV |
SchemaVariableFactory.createModalOperatorSV(Name name,
Sort sort,
ImmutableSet<Modality> modalities)
creates a SchemaVariable representing an operator
|
static SkolemTermSV |
SchemaVariableFactory.createSkolemTermSV(Name name,
Sort s)
creates a SchemaVariable representing a skolem term
|
static TermSV |
SchemaVariableFactory.createTermSV(Name name,
Sort sort) |
static TermSV |
SchemaVariableFactory.createTermSV(Name name,
Sort sort,
boolean rigidness,
boolean strictSV)
creates a SchemaVariable representing a term but not a formula
|
static VariableSV |
SchemaVariableFactory.createVariableSV(Name name,
Sort sort)
creates a SchemaVariable representing quantified variables
|
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.
|
Modifier and Type | Method and Description |
---|---|
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.
|
Constructor and Description |
---|
AbstractSortedOperator(Name name,
ImmutableArray<Sort> argSorts,
Sort sort,
boolean isRigid) |
AbstractSortedOperator(Name name,
ImmutableArray<Sort> argSorts,
Sort sort,
ImmutableArray<java.lang.Boolean> whereToBind,
boolean isRigid) |
AbstractSortedOperator(Name name,
Sort[] argSorts,
Sort sort,
boolean isRigid) |
AbstractSortedOperator(Name name,
Sort[] argSorts,
Sort sort,
boolean isRigid) |
AbstractSortedOperator(Name name,
Sort[] argSorts,
Sort sort,
java.lang.Boolean[] whereToBind,
boolean isRigid) |
AbstractSortedOperator(Name name,
Sort[] argSorts,
Sort sort,
java.lang.Boolean[] whereToBind,
boolean isRigid) |
AbstractSortedOperator(Name name,
Sort sort,
boolean isRigid) |
AbstractSV(Name name,
ImmutableArray<Sort> argSorts,
Sort sort,
boolean isRigid,
boolean isStrict) |
AbstractSV(Name name,
Sort[] argSorts,
Sort sort,
boolean isRigid,
boolean isStrict) |
AbstractSV(Name name,
Sort[] argSorts,
Sort sort,
boolean isRigid,
boolean isStrict) |
AbstractSV(Name name,
Sort sort,
boolean isRigid,
boolean isStrict) |
AbstractTermTransformer(Name name,
int arity,
Sort sort) |
Function(Name name,
Sort sort) |
Function(Name name,
Sort sort,
boolean isSkolemConstant) |
Function(Name name,
Sort sort,
boolean isSkolemConstant,
Sort... argSorts) |
Function(Name name,
Sort sort,
boolean isSkolemConstant,
Sort... argSorts) |
Function(Name name,
Sort sort,
ImmutableArray<Sort> argSorts) |
Function(Name name,
Sort sort,
ImmutableArray<Sort> argSorts,
ImmutableArray<java.lang.Boolean> whereToBind,
boolean unique) |
Function(Name name,
Sort sort,
ImmutableArray<Sort> argSorts,
ImmutableArray<java.lang.Boolean> whereToBind,
boolean unique,
boolean isSkolemConstant) |
Function(Name name,
Sort sort,
Sort... argSorts) |
Function(Name name,
Sort sort,
Sort... argSorts) |
Function(Name name,
Sort sort,
Sort[] argSorts,
java.lang.Boolean[] whereToBind,
boolean unique) |
Function(Name name,
Sort sort,
Sort[] argSorts,
java.lang.Boolean[] whereToBind,
boolean unique) |
Function(Name name,
Sort sort,
Sort[] argSorts,
java.lang.Boolean[] whereToBind,
boolean unique,
boolean isSkolemConstant) |
Function(Name name,
Sort sort,
Sort[] argSorts,
java.lang.Boolean[] whereToBind,
boolean unique,
boolean isSkolemConstant) |
LocationVariable(ProgramElementName name,
Sort s) |
LogicVariable(Name name,
Sort sort) |
ObserverFunction(java.lang.String baseName,
Sort sort,
KeYJavaType type,
Sort heapSort,
KeYJavaType container,
boolean isStatic,
ImmutableArray<KeYJavaType> paramTypes,
int heapCount,
int stateCount) |
ProgramMethod(MethodDeclaration method,
KeYJavaType container,
KeYJavaType kjt,
PositionInfo pi,
Sort heapSort) |
ProgramMethod(MethodDeclaration method,
KeYJavaType container,
KeYJavaType kjt,
PositionInfo pi,
Sort heapSort,
int heapCount) |
ProgramVariable(ProgramElementName name,
Sort s,
KeYJavaType t,
KeYJavaType containingType,
boolean isStatic,
boolean isModel,
boolean isGhost) |
ProgramVariable(ProgramElementName name,
Sort s,
KeYJavaType t,
KeYJavaType containingType,
boolean isStatic,
boolean isModel,
boolean isGhost,
boolean isFinal) |
Transformer(Name name,
Sort argSort) |
Transformer(Name name,
Sort sort,
ImmutableArray<Sort> argSorts) |
Constructor and Description |
---|
AbstractSortedOperator(Name name,
ImmutableArray<Sort> argSorts,
Sort sort,
boolean isRigid) |
AbstractSortedOperator(Name name,
ImmutableArray<Sort> argSorts,
Sort sort,
ImmutableArray<java.lang.Boolean> whereToBind,
boolean isRigid) |
AbstractSV(Name name,
ImmutableArray<Sort> argSorts,
Sort sort,
boolean isRigid,
boolean isStrict) |
Function(Name name,
Sort sort,
ImmutableArray<Sort> argSorts) |
Function(Name name,
Sort sort,
ImmutableArray<Sort> argSorts,
ImmutableArray<java.lang.Boolean> whereToBind,
boolean unique) |
Function(Name name,
Sort sort,
ImmutableArray<Sort> argSorts,
ImmutableArray<java.lang.Boolean> whereToBind,
boolean unique,
boolean isSkolemConstant) |
Transformer(Name name,
Sort sort,
ImmutableArray<Sort> argSorts) |
Modifier and Type | Class and Description |
---|---|
class |
AbstractSort
Abstract base class for implementations of the Sort interface.
|
class |
ArraySort
The objects of this class represent array sorts (in the sense of *Java*
arrays).
|
class |
GenericSort
Sort used for generic taclets
Within an SVInstantiations-object a generic sort is instantiated by
a concrete sort, which has to be a subsort of the instantiations of
the supersorts of this sort
|
class |
NullSort
There is one instance of this class per proof, representing the sort "Null".
|
class |
ProgramSVSort
Special "sorts" used for schema variables matching program constructs
(class ProgramSV).
|
static class |
ProgramSVSort.SimpleExpressionNonStringObjectSort
This sort represents a type of program schema variables that match
on non string object variables.
|
static class |
ProgramSVSort.SimpleExpressionStringSort
This sort represents a type of program schema variables that match
on string literals and string variables.
|
class |
ProxySort |
class |
SortImpl
Standard implementation of the Sort interface.
|
Modifier and Type | Field and Description |
---|---|
static Sort |
Sort.ANY
Any is a supersort of all sorts.
|
static Sort |
Sort.FORMULA
Formulas are represented as "terms" of this sort.
|
static Sort |
Sort.TERMLABEL
Term labels are represented as "terms" of this sort.
|
static Sort |
Sort.UPDATE
Updates are represented as "terms" of this sort.
|
Modifier and Type | Method and Description |
---|---|
Sort |
ArraySort.elementSort()
returns the element sort of the array
|
static Sort |
ArraySort.getArraySortForDim(Sort elemSort,
Type elemType,
int n,
Sort objectSort,
Sort cloneableSort,
Sort serializableSort)
returns elemSort([])^n.
|
Sort |
GenericSupersortException.getIllegalSort() |
Modifier and Type | Method and Description |
---|---|
ImmutableSet<Sort> |
NullSort.extendsSorts() |
ImmutableSet<Sort> |
AbstractSort.extendsSorts() |
ImmutableSet<Sort> |
Sort.extendsSorts() |
ImmutableSet<Sort> |
NullSort.extendsSorts(Services services) |
ImmutableSet<Sort> |
AbstractSort.extendsSorts(Services services) |
ImmutableSet<Sort> |
Sort.extendsSorts(Services services) |
ImmutableSet<Sort> |
GenericSort.getOneOf() |
Modifier and Type | Method and Description |
---|---|
protected boolean |
GenericSort.checkNonGenericSupersorts(Sort p_s) |
boolean |
NullSort.extendsTrans(Sort sort) |
boolean |
AbstractSort.extendsTrans(Sort sort) |
boolean |
Sort.extendsTrans(Sort s) |
static ArraySort |
ArraySort.getArraySort(Sort elemSort,
Sort objectSort,
Sort cloneableSort,
Sort serializableSort) |
static ArraySort |
ArraySort.getArraySort(Sort elemSort,
Type elemType,
Sort objectSort,
Sort cloneableSort,
Sort serializableSort)
Returns the ArraySort to the given element sort and element type.
|
static Sort |
ArraySort.getArraySortForDim(Sort elemSort,
Type elemType,
int n,
Sort objectSort,
Sort cloneableSort,
Sort serializableSort)
returns elemSort([])^n.
|
boolean |
GenericSort.isPossibleInstantiation(Sort p_s) |
Constructor and Description |
---|
GenericSupersortException(java.lang.String description,
Sort illegalSort) |
NullSort(Sort objectSort) |
SortImpl(Name name,
Sort ext) |
Constructor and Description |
---|
AbstractSort(Name name,
ImmutableSet<Sort> ext,
boolean isAbstract) |
GenericSort(Name name,
ImmutableSet<Sort> ext,
ImmutableSet<Sort> oneOf)
creates a generic sort
|
GenericSort(Name name,
ImmutableSet<Sort> ext,
ImmutableSet<Sort> oneOf)
creates a generic sort
|
ProxySort(Name name,
ImmutableSet<Sort> ext) |
SortImpl(Name name,
ImmutableSet<Sort> ext) |
SortImpl(Name name,
ImmutableSet<Sort> ext,
boolean isAbstract) |
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 |
---|---|
Sort |
EngineState.toSort(java.lang.String sortName) |
Modifier and Type | Method and Description |
---|---|
Term |
EngineState.toTerm(java.lang.String string,
Sort sort) |
Modifier and Type | Method and Description |
---|---|
protected Sort |
DefaultBuilder.lookupSort(java.lang.String name)
looks up and returns the sort of the given name or null if none has been found.
|
Sort |
DefaultBuilder.toArraySort(Pair<Sort,Type> p,
int numOfDimensions) |
Sort |
DefaultBuilder.visitArg_sorts_or_formula_helper(KeYParser.Arg_sorts_or_formula_helperContext ctx) |
Sort |
DefaultBuilder.visitSortId(KeYParser.SortIdContext ctx) |
Modifier and Type | Method and Description |
---|---|
protected Namespace<Sort> |
DefaultBuilder.sorts() |
java.util.List<Sort> |
DefaultBuilder.visitArg_sorts_or_formula(KeYParser.Arg_sorts_or_formulaContext ctx) |
java.util.List<Sort> |
DefaultBuilder.visitArg_sorts(KeYParser.Arg_sortsContext ctx) |
java.util.List<Sort> |
DeclarationBuilder.visitExtends_sorts(KeYParser.Extends_sortsContext ctx) |
java.util.List<Sort> |
DeclarationBuilder.visitOneof_sorts(KeYParser.Oneof_sortsContext ctx) |
Modifier and Type | Method and Description |
---|---|
protected void |
TacletPBuilder.declareSchemaVariable(org.antlr.v4.runtime.ParserRuleContext ctx,
java.lang.String name,
Sort s,
boolean makeVariableSV,
boolean makeSkolemTermSV,
boolean makeTermLabelSV,
SchemaVariableModifierSet mods) |
protected Operator |
DefaultBuilder.lookupVarfuncId(org.antlr.v4.runtime.ParserRuleContext ctx,
java.lang.String varfuncName,
java.lang.String sortName,
Sort sort)
looks up a function, (program) variable or static query of the
given name varfunc_id and the argument terms args in the namespaces
and java info.
|
Modifier and Type | Method and Description |
---|---|
Sort |
DefaultBuilder.toArraySort(Pair<Sort,Type> p,
int numOfDimensions) |
Modifier and Type | Method and Description |
---|---|
Sort |
IdDeclaration.getSort() |
Modifier and Type | Method and Description |
---|---|
Term |
DefaultTermParser.parse(java.io.Reader in,
Sort sort,
Services services,
Namespace<QuantifiableVariable> var_ns,
Namespace<Function> func_ns,
Namespace<Sort> sort_ns,
Namespace<IProgramVariable> progVar_ns,
AbbrevMap scm)
Deprecated.
The method reads the input and parses a term with the
specified namespaces.
|
Term |
DefaultTermParser.parse(java.io.Reader in,
Sort sort,
Services services,
NamespaceSet nss,
AbbrevMap scm)
Deprecated.
The method reads the input and parses a term with the
specified namespaces.
|
Modifier and Type | Method and Description |
---|---|
Term |
DefaultTermParser.parse(java.io.Reader in,
Sort sort,
Services services,
Namespace<QuantifiableVariable> var_ns,
Namespace<Function> func_ns,
Namespace<Sort> sort_ns,
Namespace<IProgramVariable> progVar_ns,
AbbrevMap scm)
Deprecated.
The method reads the input and parses a term with the
specified namespaces.
|
Constructor and Description |
---|
GenericSortException(java.lang.String cat,
java.lang.String reason,
Sort sort,
java.lang.String filename,
int line,
int column) |
GenericSortException(java.lang.String cat,
java.lang.String reason,
Sort sort,
antlr.Token t,
java.lang.String filename) |
IdDeclaration(java.lang.String p_name,
Sort p_sort) |
Modifier and Type | Method and Description |
---|---|
boolean |
LogicPrinter.printInShortForm(java.lang.String programName,
Sort sort)
tests if the program name together with the prefix sort determines the
attribute in a unique way
|
static boolean |
LogicPrinter.printInShortForm(java.lang.String programName,
Sort sort,
Services services)
tests if the program name together with the prefix sort determines the
attribute in a unique way
|
Constructor and Description |
---|
SortMismatchException(java.lang.String toInstantiate,
Sort givenSort,
int row,
int column) |
Modifier and Type | Method and Description |
---|---|
Namespace<Sort> |
InitConfig.sortNS()
returns the sort namespace of this initial configuration
|
Modifier and Type | Method and Description |
---|---|
Sort |
TacletApp.getRealSort(SchemaVariable p_sv,
TermServices services) |
Modifier and Type | Method and Description |
---|---|
TacletApp |
TacletApp.createSkolemConstant(java.lang.String instantiation,
SchemaVariable sv,
Sort sort,
boolean interesting,
Services services) |
Modifier and Type | Method and Description |
---|---|
Sort |
TypeResolver.NonGenericSortResolver.getSort() |
abstract Sort |
TypeResolver.resolveSort(SchemaVariable sv,
SVSubstitute instCandidate,
SVInstantiations instMap,
Services services) |
Sort |
TypeResolver.GenericSortResolver.resolveSort(SchemaVariable sv,
SVSubstitute instCandidate,
SVInstantiations instMap,
Services services) |
Sort |
TypeResolver.NonGenericSortResolver.resolveSort(SchemaVariable sv,
SVSubstitute instCandidate,
SVInstantiations instMap,
Services services) |
Sort |
TypeResolver.ElementTypeResolverForSV.resolveSort(SchemaVariable sv,
SVSubstitute instCandidate,
SVInstantiations instMap,
Services services) |
Sort |
TypeResolver.ContainerTypeResolver.resolveSort(SchemaVariable sv,
SVSubstitute instCandidate,
SVInstantiations instMap,
Services services) |
Modifier and Type | Method and Description |
---|---|
static TypeResolver |
TypeResolver.createNonGenericSortResolver(Sort s) |
Constructor and Description |
---|
NonGenericSortResolver(Sort s) |
Modifier and Type | Method and Description |
---|---|
Sort |
GenericSortInstantiations.getInstantiation(GenericSort p_gs) |
Sort |
GenericSortInstantiations.getRealSort(SchemaVariable p_sv,
TermServices services) |
Sort |
GenericSortInstantiations.getRealSort(Sort p_s,
TermServices services) |
Modifier and Type | Method and Description |
---|---|
ImmutableMap<GenericSort,Sort> |
GenericSortInstantiations.getAllInstantiations()
ONLY FOR JUNIT TESTS
|
Modifier and Type | Method and Description |
---|---|
abstract boolean |
GenericSortCondition.check(Sort s,
GenericSortInstantiations insts)
returns true if the given sort
s satisfies this generic sort
condition |
protected static GenericSortCondition |
GenericSortCondition.createCondition(Sort s0,
Sort s1,
boolean p_identity)
Create the condition to make a generic sort (s0) (or a
collection sort of a generic sort) and a concrete sort (s1)
equal
|
static GenericSortCondition |
GenericSortCondition.createIdentityCondition(GenericSort p_gs,
Sort p_s) |
static GenericSortCondition |
GenericSortCondition.createSupersortCondition(GenericSort p_gs,
Sort p_s) |
static GenericSortCondition |
GenericSortCondition.forceInstantiation(Sort p_s,
boolean p_maximum)
Create the condition to force the instantiation of a given
(possibly generic) sort
|
Sort |
GenericSortInstantiations.getRealSort(Sort p_s,
TermServices services) |
Modifier and Type | Method and Description |
---|---|
java.util.HashMap<Sort,java.util.ArrayList<AbstractionPredicate>> |
MergeWithPredicateAbstraction.getPredicates() |
Modifier and Type | Method and Description |
---|---|
protected abstract AbstractDomainLattice |
MergeWithLatticeAbstraction.getAbstractDomainForSort(Sort s,
Services services)
Returns the abstract domain lattice for the given sort or null if there
has no lattice been specified for that sort.
|
AbstractDomainLattice |
MergeWithPredicateAbstraction.getAbstractDomainForSort(Sort s,
Services services) |
static AbstractDomainLattice |
MergeWithPredicateAbstraction.instantiateAbstractDomain(Sort s,
java.util.List<AbstractionPredicate> applicablePredicates,
java.lang.Class<? extends AbstractPredicateAbstractionLattice> latticeType,
Services services)
Instantiates the abstract domain lattice for the given sort or null if
there has no lattice been specified for that sort.
|
Modifier and Type | Method and Description |
---|---|
void |
MergeWithPredicateAbstraction.setPredicates(java.util.HashMap<Sort,java.util.ArrayList<AbstractionPredicate>> predicates) |
Modifier and Type | Method and Description |
---|---|
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) |
ImmutableSet<Taclet> |
TacletGenerator.generateFunctionalRepresentsTaclets(Name name,
Term originalPreTerm,
Term originalRepresentsTerm,
KeYJavaType kjt,
IObserverFunction target,
java.util.List<? extends ProgramVariable> heaps,
ProgramVariable self,
ImmutableList<ProgramVariable> paramVars,
java.util.Map<LocationVariable,ProgramVariable> atPreVars,
ImmutableSet<Pair<Sort,IObserverFunction>> toLimit,
boolean satisfiability,
Services services) |
ImmutableSet<Taclet> |
TacletGenerator.generatePartialInvTaclet(Name name,
java.util.List<SchemaVariable> heapSVs,
SchemaVariable selfSV,
SchemaVariable eqSV,
Term term,
KeYJavaType kjt,
ImmutableSet<Pair<Sort,IObserverFunction>> toLimit,
boolean isStatic,
boolean eqVersion,
Services services) |
Modifier and Type | Field and Description |
---|---|
protected java.util.HashMap<Sort,java.lang.StringBuffer> |
AbstractSMTTranslator.usedDisplaySort |
protected java.util.HashMap<Sort,java.lang.StringBuffer> |
AbstractSMTTranslator.usedRealSort |
Modifier and Type | Method and Description |
---|---|
Sort |
ProblemTypeInformation.getOriginalConstantType(java.lang.String c) |
Modifier and Type | Method and Description |
---|---|
java.util.Set<Sort> |
ProblemTypeInformation.getJavaSorts() |
Modifier and Type | Method and Description |
---|---|
java.util.Set<java.lang.String> |
ProblemTypeInformation.getFieldsForSort(Sort s)
Return a list of field names for the specified sort.
|
protected java.lang.StringBuffer |
AbstractSMTTranslator.getTypePredicate(Sort s,
java.lang.StringBuffer arg)
Get the type predicate for the given sort and the given expression.
|
protected boolean |
AbstractSMTTranslator.isSomeIntegerSort(Sort s) |
void |
ProblemTypeInformation.putOriginalConstantType(java.lang.String c,
Sort s) |
protected java.lang.StringBuffer |
AbstractSMTTranslator.translateLogicalAll(java.lang.StringBuffer var,
Sort sort,
java.lang.StringBuffer result) |
Modifier and Type | Method and Description |
---|---|
void |
ProblemTypeInformation.setJavaSorts(java.util.Set<Sort> javaSorts) |
protected java.lang.StringBuffer |
AbstractSMTTranslator.translateLogicalAll(java.util.ArrayList<java.lang.StringBuffer> variables,
java.util.ArrayList<Sort> sorts,
java.lang.StringBuffer result) |
Constructor and Description |
---|
SortHierarchy(java.util.HashMap<Sort,java.lang.StringBuffer> sortnames,
java.util.HashMap<Sort,java.lang.StringBuffer> prednames,
boolean explicitNullHierarchy,
boolean explicitHierarchy,
Services services)
Create a Sort Hierarchy.
|
SortHierarchy(java.util.HashMap<Sort,java.lang.StringBuffer> sortnames,
java.util.HashMap<Sort,java.lang.StringBuffer> prednames,
boolean explicitNullHierarchy,
boolean explicitHierarchy,
Services services)
Create a Sort Hierarchy.
|
Modifier and Type | Method and Description |
---|---|
Sort |
SortNode.getSort() |
Modifier and Type | Method and Description |
---|---|
java.util.List<Sort> |
TypeHierarchy.getArraySortList() |
java.util.List<Sort> |
TypeHierarchy.getSortList() |
Modifier and Type | Method and Description |
---|---|
java.util.Set<SortNode> |
TypeHierarchy.getChildren(Sort s)
Returns the children of a sort s.
|
java.util.Set<SortNode> |
TypeHierarchy.getParents(Sort s)
Returns the parents of a sort s.
|
Constructor and Description |
---|
SortNode(Sort sort) |
Modifier and Type | Method and Description |
---|---|
Sort |
ObjectVal.getSort()
queries the sort of this entity
|
Modifier and Type | Method and Description |
---|---|
void |
ObjectVal.setSort(Sort sort)
sets the sort of this object/array/function
|
Modifier and Type | Method and Description |
---|---|
java.util.Set<Sort> |
MasterHandler.getSorts() |
Modifier and Type | Method and Description |
---|---|
void |
MasterHandler.addSort(Sort s) |
static SExpr |
LogicalVariableHandler.makeVarDecl(java.lang.String name,
Sort sort) |
static SExpr |
LogicalVariableHandler.makeVarRef(java.lang.String name,
Sort sort) |
static SExpr |
SExprs.sortExpr(Sort sort)
Turn a KeY sort into an SMT sort (by prefixing
SExprs.SORT_PREFIX . |
Modifier and Type | Method and Description |
---|---|
abstract ImmutableSet<Pair<Sort,IObserverFunction>> |
ClassAxiom.getUsedObservers(Services services)
Returns the pairs (kjt, obs) for which there is an occurrence of
o.obs in the axiom, where kjt is the type of o (excluding the
defining occurrence of the axiom target).
|
ImmutableSet<Pair<Sort,IObserverFunction>> |
ClassAxiomImpl.getUsedObservers(Services services) |
ImmutableSet<Pair<Sort,IObserverFunction>> |
QueryAxiom.getUsedObservers(Services services) |
ImmutableSet<Pair<Sort,IObserverFunction>> |
PartialInvAxiom.getUsedObservers(Services services) |
ImmutableSet<Pair<Sort,IObserverFunction>> |
ContractAxiom.getUsedObservers(Services services) |
ImmutableSet<Pair<Sort,IObserverFunction>> |
RepresentsAxiom.getUsedObservers(Services services) |
ImmutableSet<Pair<Sort,IObserverFunction>> |
ModelMethodExecution.getUsedObservers(Services services) |
Modifier and Type | Method and Description |
---|---|
abstract ImmutableSet<Taclet> |
ClassAxiom.getTaclets(ImmutableSet<Pair<Sort,IObserverFunction>> toLimit,
Services services)
The axiom as one or many taclets, where the non-defining occurrences of
the passed observers are replaced by their "limited" counterparts.
|
ImmutableSet<Taclet> |
ClassAxiomImpl.getTaclets(ImmutableSet<Pair<Sort,IObserverFunction>> toLimit,
Services services) |
ImmutableSet<Taclet> |
QueryAxiom.getTaclets(ImmutableSet<Pair<Sort,IObserverFunction>> toLimit,
Services services) |
ImmutableSet<Taclet> |
PartialInvAxiom.getTaclets(ImmutableSet<Pair<Sort,IObserverFunction>> toLimit,
Services services) |
ImmutableSet<Taclet> |
ContractAxiom.getTaclets(ImmutableSet<Pair<Sort,IObserverFunction>> toLimit,
Services services) |
ImmutableSet<Taclet> |
RepresentsAxiom.getTaclets(ImmutableSet<Pair<Sort,IObserverFunction>> toLimit,
Services services) |
ImmutableSet<Taclet> |
ModelMethodExecution.getTaclets(ImmutableSet<Pair<Sort,IObserverFunction>> toLimit,
Services services) |
Modifier and Type | Method and Description |
---|---|
protected static TermFeature |
StaticFeatureCollection.extendsTrans(Sort s) |
Modifier and Type | Method and Description |
---|---|
protected boolean |
SortComparisonFeature.compare(Sort sort1,
Sort sort2) |
Constructor and Description |
---|
Metavariable(Name name,
Sort sort)
Deprecated.
|
Modifier and Type | Method and Description |
---|---|
static TermFeature |
SortExtendsTransTermFeature.create(Sort sort) |
Modifier and Type | Method and Description |
---|---|
Sort |
ExecutionNodeReader.KeYlessTermination.getExceptionSort()
Returns the
Sort of the caught exception. |
Sort |
SymbolicLayoutReader.KeYlessObject.getType()
Returns the type of this object.
|
Sort |
SymbolicLayoutReader.KeYlessValue.getType()
Returns the type of the value.
|
Modifier and Type | Method and Description |
---|---|
protected LocationVariable |
AbstractUpdateExtractor.ExtractLocationParameter.createLocationVariable(java.lang.String name,
Sort sort)
Creates a new
LocationVariable with the given name and Sort . |
Modifier and Type | Method and Description |
---|---|
Sort |
IExecutionTermination.getExceptionSort()
Returns the
Sort of the caught exception. |
Modifier and Type | Method and Description |
---|---|
Sort |
ExecutionTermination.getExceptionSort()
Returns the
Sort of the caught exception. |
Modifier and Type | Method and Description |
---|---|
Sort |
ISymbolicObject.getType()
Returns the type of this object.
|
Sort |
ISymbolicValue.getType()
Returns the type of the value.
|
Modifier and Type | Method and Description |
---|---|
Sort |
SymbolicValue.getType()
Returns the type of the value.
|
Sort |
SymbolicObject.getType()
Returns the type of this object.
|
Modifier and Type | Method and Description |
---|---|
protected Function |
AbstractSideProofRule.createResultConstant(Services services,
Sort sort)
Creates a constant which is used in the original
Proof to
store the computed result in form of QueryResult = ... |
protected Function |
AbstractSideProofRule.createResultFunction(Services services,
Sort sort)
Creates the result
Function used in a predicate to compute the result in the side proof. |
Modifier and Type | Method and Description |
---|---|
static Sort |
SymbolicExecutionUtil.lazyComputeExceptionSort(Node node,
IProgramVariable exceptionVariable)
Computes the exception
Sort lazily when #getExceptionSort()
is called the first time. |
Modifier and Type | Method and Description |
---|---|
static boolean |
SymbolicExecutionUtil.hasReferenceSort(Services services,
Sort sort)
Checks if the
Sort is a reference type. |
static boolean |
SymbolicExecutionUtil.isNullSort(Sort sort,
Services services)
|
Modifier and Type | Method and Description |
---|---|
static void |
AssumptionGenerator.checkTable(byte[][] referenceTable,
Sort[] instTable,
Sort[] genericTable,
de.uka.ilkd.key.taclettranslation.assumptions.TacletConditions conditions,
Services services)
Checks the referenceTable whether there are rows that are not
allowed.
|
static void |
AssumptionGenerator.checkTable(byte[][] referenceTable,
Sort[] instTable,
Sort[] genericTable,
de.uka.ilkd.key.taclettranslation.assumptions.TacletConditions conditions,
Services services)
Checks the referenceTable whether there are rows that are not
allowed.
|
boolean |
DefaultTacletSetTranslation.eventInstantiationFailure(GenericSort dest,
Sort sort,
Taclet t,
Term term) |
boolean |
TranslationListener.eventInstantiationFailure(GenericSort dest,
Sort sort,
Taclet t,
Term term)
Called when the translator can not instantiate a generic sort
with a particular sort in the given term.
|
void |
DefaultTacletSetTranslation.eventSort(Sort sort) |
void |
TranslationListener.eventSort(Sort sort)
Called when the translator finds a term that have a sort.
|
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.
|
static boolean |
AssumptionGenerator.isAbstractOrInterface(Sort sort,
Services services) |
static boolean |
AssumptionGenerator.isReferenceSort(Sort sort,
Services services) |
Modifier and Type | Method and Description |
---|---|
ImmutableList<TacletFormula> |
TacletSetTranslation.getTranslation(ImmutableSet<Sort> sorts)
Builds the translation of the taclets given by calling the method
setTacletSet() . |
ImmutableList<TacletFormula> |
DefaultTacletSetTranslation.getTranslation(ImmutableSet<Sort> sorts) |
TacletFormula |
AssumptionGenerator.translate(Taclet t,
ImmutableSet<Sort> sorts,
int maxGeneric) |
Modifier and Type | Method and Description |
---|---|
protected Sort |
GenericRemovingLemmaGenerator.replaceSort(Sort sort,
TermServices services)
Sometimes sorts must be replaced during lemma generation.
|
Modifier and Type | Method and Description |
---|---|
java.util.Map<Name,Sort> |
UserDefinedSymbols.getExtraSorts() |
Modifier and Type | Method and Description |
---|---|
protected Sort |
GenericRemovingLemmaGenerator.replaceSort(Sort sort,
TermServices services)
Sometimes sorts must be replaced during lemma generation.
|
Modifier and Type | Method and Description |
---|---|
protected java.util.Map<java.lang.String,Sort> |
TestCaseGenerator.generateTypeInferenceMap(Node n) |
Modifier and Type | Method and Description |
---|---|
void |
ReflectionClassCreator.addSort(Sort s)
Constructors, setter-, getter-methods will be created for the added sorts.
|
protected java.lang.String |
TestCaseGenerator.buildDummyClassForAbstractSort(Sort sort) |
java.lang.String |
TestCaseGenerator.getSafeType(Sort sort) |
Modifier and Type | Method and Description |
---|---|
java.lang.String |
TestCaseGenerator.generateTestCase(Model m,
java.util.Map<java.lang.String,Sort> typeInfMap) |
protected java.lang.String |
TestCaseGenerator.inferSort(java.util.Map<java.lang.String,Sort> typeInfMap,
java.lang.String progVar) |
Modifier and Type | Method and Description |
---|---|
Sort |
OracleConstant.getSort() |
Sort |
OracleVariable.getSort() |
Modifier and Type | Method and Description |
---|---|
Term |
OracleInvariantTranslator.getInvariantTerm(Sort s) |
void |
OracleConstant.setSort(Sort sort) |
Constructor and Description |
---|
OracleConstant(java.lang.String value,
Sort sort) |
OracleMethod(java.lang.String methodName,
java.util.List<OracleVariable> args,
java.lang.String body,
Sort sort) |
OracleType(Sort s) |
OracleVariable(java.lang.String name,
Sort sort) |
Modifier and Type | Method and Description |
---|---|
static ImmutableSet<Pair<Sort,IObserverFunction>> |
MiscTools.collectObservers(Term t)
Recursively collect all observers for this term including all of its sub terms.
|
Modifier and Type | Method and Description |
---|---|
static Pair<Sort,Name> |
MergeRuleUtils.parsePlaceholder(java.lang.String input,
boolean registerInNamespaces,
Services services)
Parses a declaration of the type "<SORT> <NAME>", where
<SORT> must be a sort known to the proof and <NAME> must be a
fresh name.
|
static Pair<Sort,Name> |
MergeRuleUtils.parsePlaceholder(java.lang.String input,
Services services)
Parses a declaration of the type "<SORT> <NAME>", where
<SORT> must be a sort known to the proof and <NAME> must be a
fresh name.
|
Modifier and Type | Method and Description |
---|---|
static LocationVariable |
MergeRuleUtils.getFreshLocVariableForPrefix(java.lang.String prefix,
Sort sort,
Services services)
Computes and registers a fresh location variable with the given prefix in
its name of the given sort.
|
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.
|
static Function |
MergeRuleUtils.getNewSkolemConstantForPrefix(java.lang.String prefix,
Sort sort,
Services services)
Computes and registers a new Skolem constant with the given prefix in its
name of the given sort.
|
Modifier and Type | Method and Description |
---|---|
static AbstractionPredicate |
MergeRuleUtils.parsePredicate(java.lang.String input,
java.util.ArrayList<Pair<Sort,Name>> registeredPlaceholders,
NamespaceSet localNamespaces,
Services services)
Parses an abstraction predicate.
|
Copyright © 2003-2019 The KeY-Project.