de.uka.ilkd.key.util

Class KeYTypeUtil

java.lang.Object

de.uka.ilkd.key.util.KeYTypeUtil

public final class KeYTypeUtil
extends java.lang.Object

Provides utility methods which makes it easier to analyze the type hierarchy of KeYJavaType instances with help of given Services.

Author:

Martin Hentschel

Field Summary

Fields

Modifier and Type	Field and Description
static java.lang.String	PACKAGE_SEPARATOR Separator between packages and types.

Constructor Summary

Constructors

Modifier	Constructor and Description
private	KeYTypeUtil() Forbid instances.

Method Summary

Modifier and Type	Method and Description
static IProgramMethod	findExplicitConstructor(Services services, IProgramMethod implicitConstructor) Returns the IProgramMethod of the explicit constructor for the given implicit constructor.
static java.lang.String	getParentName(Services services, KeYJavaType type) Returns the name of the parent package/type or null if it has no one.
private static java.lang.String	getParentName(Services services, java.lang.String fullName) Returns the name of the parent package/type or null if it has no one.
static KeYJavaType	getType(Services services, java.lang.String fullName) Returns the KeYJavaType fore the given name.
static boolean	isImplicitConstructor(IProgramMethod pm) Checks if the given IProgramMethod is an implicit constructor.
static boolean	isInnerType(Services services, KeYJavaType type) Checks if the given type is an inner or anonymous type.
static boolean	isLibraryClass(KeYJavaType kjt) Checks if the given KeYJavaType is a library class.
static boolean	isType(Services services, java.lang.String fullName) Checks if the given full name is a type in KeY.
static java.lang.String	resolveType(ParameterDeclaration parameterDeclaration) Resolves the type of the given ParameterDeclaration.
static java.lang.String	resolveType(Type type) Resolves the type of the given Type.
static java.lang.String	resolveType(TypeReference typeReference) Resolves the type of the given TypeReference.

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

PACKAGE_SEPARATOR

public static final java.lang.String PACKAGE_SEPARATOR

Separator between packages and types.

See Also:

Constant Field Values

Constructor Detail

KeYTypeUtil

private KeYTypeUtil()

Forbid instances.

Method Detail

isInnerType

public static boolean isInnerType(Services services,
                                  KeYJavaType type)

Checks if the given type is an inner or anonymous type.

Parameters:

services - The Services to use.

type - The type to check.

Returns:

true is inner or anonymous, false is not

getParentName

public static java.lang.String getParentName(Services services,
                                             KeYJavaType type)

Returns the name of the parent package/type or null if it has no one.

Parameters:

services - The Services to use.

type - The type.

Returns:

The parent package/type or null if it has no one.

getParentName

private static java.lang.String getParentName(Services services,
                                              java.lang.String fullName)

Returns the name of the parent package/type or null if it has no one.

Parameters:

services - The Services to use.

fullName - The name of the current package/type.

Returns:

The parent package/type or null if it has no one.

isType

public static boolean isType(Services services,
                             java.lang.String fullName)

Checks if the given full name is a type in KeY.

Parameters:

services - The services to use.

fullName - The full name to check.

Returns:

true = is type, false = is no type

getType

public static KeYJavaType getType(Services services,
                                  java.lang.String fullName)

Returns the KeYJavaType fore the given name.

Parameters:

services - The Services to use.

fullName - The full name of the requested KeYJavaType.

Returns:

The found KeYJavaType or null if no type exist with the given name.

isLibraryClass

public static boolean isLibraryClass(KeYJavaType kjt)

Checks if the given KeYJavaType is a library class.

Parameters:

kjt - The KeYJavaType to check.

Returns:

true is library class, false is no library class.

isImplicitConstructor

public static boolean isImplicitConstructor(IProgramMethod pm)

Checks if the given IProgramMethod is an implicit constructor.

Parameters:

pm - The IProgramMethod to check.

Returns:

true is implicit constructor, false is no implicit constructor (e.g. method or explicit construcotr).

findExplicitConstructor

public static IProgramMethod findExplicitConstructor(Services services,
                                                     IProgramMethod implicitConstructor)

Returns the IProgramMethod of the explicit constructor for the given implicit constructor.

Parameters:

services - The Services to use.

implicitConstructor - The implicit constructor.

Returns:

The found explicit constructor or null if not available.

resolveType

public static java.lang.String resolveType(ParameterDeclaration parameterDeclaration)

Resolves the type of the given ParameterDeclaration.

Parameters:

parameterDeclaration - The ParameterDeclaration to resolve.

Returns:

The full qualified type name or null if the given ParameterDeclaration is null.

resolveType

public static java.lang.String resolveType(TypeReference typeReference)

Resolves the type of the given TypeReference.

Parameters:

typeReference - The TypeReference to resolve.

Returns:

The full qualified type name or null if the given TypeReference is null.

resolveType

public static java.lang.String resolveType(Type type)

Resolves the type of the given Type.

Parameters:

type - The Type to resolve.

Returns:

The full qualified type name or null if the given Type is null.