Package | Description |
---|---|
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.java.declaration |
Elements of the Java syntax tree representing declarations.
|
de.uka.ilkd.key.ldt |
This package contains the "language data types" (LDTs) of KeY.
|
de.uka.ilkd.key.logic.sort |
This package contains different kinds and implementations subtyping interface Sort.
|
de.uka.ilkd.key.nparser.builder | |
de.uka.ilkd.key.speclang.jml | |
de.uka.ilkd.key.util |
This package is a grab bag of miscellaneous useful code fragments.
|
Modifier and Type | Field and Description |
---|---|
protected Type |
PrettyPrinter.classToPrint
Enforces the output of real Java syntax that can be compiled.
|
Modifier and Type | Method and Description |
---|---|
ImmutableList<KeYJavaType> |
KeYProgModelInfo.findImplementations(Type ct,
java.lang.String name,
ImmutableList<KeYJavaType> signature) |
protected Expression |
CreateArrayMethodBuilder.getDefaultValue(Type type)
returns the default value of the given type according to JLS \S 4.5.5
|
KeYJavaType |
JavaInfo.getKeYJavaType(Type t)
returns the KeYJavaType belonging to the given Type t
|
KeYJavaType |
TypeConverter.getKeYJavaType(Type t) |
Sort |
TypeConverter.getPrimitiveSort(Type t) |
boolean |
TypeConverter.isAssignableTo(Expression expr,
Type to,
ExecutionContext ec) |
boolean |
TypeConverter.isAssignableTo(Type from,
Type to) |
boolean |
TypeConverter.isBooleanType(Type t) |
boolean |
TypeConverter.isCastingTo(Type from,
Type to) |
boolean |
TypeConverter.isIdentical(Type from,
Type to) |
boolean |
TypeConverter.isIntegerType(Type t2) |
boolean |
TypeConverter.isIntegralType(Type t) |
boolean |
TypeConverter.isNarrowing(Type from,
Type to) |
boolean |
TypeConverter.isNullType(Type t) |
boolean |
TypeConverter.isNumericalType(Type t) |
boolean |
TypeConverter.isReferenceType(Type t) |
boolean |
TypeConverter.isWidening(Type from,
Type to) |
static VariableSpecification |
KeYJavaASTFactory.variableSpecification(IProgramVariable variable,
int dimensions,
Expression initializer,
Type type)
Create a variable specification.
|
Modifier and Type | Method and Description |
---|---|
ImmutableList<Method> |
KeYProgModelInfo.getMethods(KeYJavaType ct,
java.lang.String m,
ImmutableList<Type> signature,
KeYJavaType context)
Returns the list of most specific methods with the given
name that are defined in the given type or in a supertype
where they are visible for the given type, and have a signature
that is compatible to the given one.
|
IProgramMethod |
JavaInfo.getProgramMethod(KeYJavaType classType,
java.lang.String methodName,
ImmutableArray<? extends Type> signature,
KeYJavaType context) |
IProgramMethod |
JavaInfo.getProgramMethod(KeYJavaType classType,
java.lang.String methodName,
ImmutableList<? extends Type> signature,
KeYJavaType context)
returns the program methods defined in the given KeYJavaType with name
m and the list of types as signature of the method
|
IProgramMethod |
KeYProgModelInfo.getProgramMethod(KeYJavaType ct,
java.lang.String m,
ImmutableList<? extends Type> signature,
KeYJavaType context)
Returns the IProgramMethods with the given name that is defined
in the given type or in a supertype where it is visible for the
given type, and has a signature that is compatible to the given one.
|
Modifier and Type | Interface and Description |
---|---|
interface |
ArrayType
A program model element representing array types.
|
interface |
ClassType
A program model element representing class types.
|
Modifier and Type | Class and Description |
---|---|
class |
KeYJavaType
The KeY java type realises a tuple (sort, type) of a logic sort and
the java type (for example a class declaration).
|
class |
NullType
A program model element representing the null type.
|
class |
PrimitiveType
A program model element representing primitive types.
|
Modifier and Type | Method and Description |
---|---|
Type |
KeYJavaType.getJavaType() |
Type |
DefaultConstructor.getReturnType()
Deprecated.
Returns the return type of this method.
|
Type[] |
DefaultConstructor.getSignature()
Deprecated.
TO BE IMPLEMENTED
Returns the signature of this constructor.
|
Type |
Variable.getType()
Returns the type of this variable.
|
Modifier and Type | Method and Description |
---|---|
void |
KeYJavaType.setJavaType(Type type) |
Constructor and Description |
---|
KeYJavaType(Type type)
creates a new KeYJavaType
|
KeYJavaType(Type javaType,
Sort sort)
creates a new KeYJavaType
|
Modifier and Type | Class and Description |
---|---|
class |
ArrayDeclaration
KeY used to model arrays using only the
ArrayType . |
class |
ClassDeclaration
There are several types of class declarations:
package-less outer classes
getClassContainer() == null
getStatementContainer() == null
getName() != null
ordinary outer classes
getClassContainer() instanceof Package
getStatementContainer() == null
getName() != null
member classes
getClassContainer() instanceof ClassDeclaration
getStatementContainer() == null
getName() != null
local class
getClassContainer() == null
getStatementContainer() != null
getName() != null
local anonymous class
getClassContainer() == null
getStatementContainer() instanceof expression.New
getName() == null
Anonymous local classes have exactly one supertype and no
subtypes.
|
class |
EnumClassDeclaration
This class is used for wrapping an enum into a standard class type.
|
class |
InterfaceDeclaration
Interface declaration.
|
class |
SuperArrayDeclaration
At the moment the mere purpose of this Class is to provide an encapsulation
for the length attribute.
|
class |
TypeDeclaration
Type declaration.
|
Modifier and Type | Field and Description |
---|---|
protected Type |
VariableSpecification.type
the type
|
Modifier and Type | Method and Description |
---|---|
Type |
VariableSpecification.getType() |
Modifier and Type | Method and Description |
---|---|
Type |
DoubleLDT.getType(Term t) |
Type |
CharListLDT.getType(Term t) |
Type |
FreeLDT.getType(Term t) |
Type |
MapLDT.getType(Term t) |
Type |
RealLDT.getType(Term t) |
Type |
BooleanLDT.getType(Term t) |
Type |
PermissionLDT.getType(Term t) |
Type |
LocSetLDT.getType(Term t) |
Type |
IntegerLDT.getType(Term t) |
Type |
HeapLDT.getType(Term t) |
Type |
FloatLDT.getType(Term t) |
Type |
SeqLDT.getType(Term t) |
abstract Type |
LDT.getType(Term t) |
Modifier and Type | Method and Description |
---|---|
Function |
IntegerLDT.getInBounds(Type t) |
Function |
IntegerLDT.getJavaCast(Type t) |
Modifier and Type | Method and Description |
---|---|
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.
|
Modifier and Type | Method and Description |
---|---|
Sort |
DefaultBuilder.toArraySort(Pair<Sort,Type> p,
int numOfDimensions) |
Modifier and Type | Method and Description |
---|---|
static int |
JMLSpecExtractor.arrayDepth(Type type,
Services services)
Get the depth for the nonNull predicate.
|
Modifier and Type | Method and Description |
---|---|
static java.lang.String |
KeYTypeUtil.resolveType(Type type)
Resolves the type of the given
Type . |
Copyright © 2003-2019 The KeY-Project.