de.uka.ilkd.key.java.declaration

Class ArrayDeclaration

java.lang.Object

de.uka.ilkd.key.java.JavaSourceElement

de.uka.ilkd.key.java.JavaProgramElement

de.uka.ilkd.key.java.JavaNonTerminalProgramElement

de.uka.ilkd.key.java.declaration.JavaDeclaration

de.uka.ilkd.key.java.declaration.TypeDeclaration

de.uka.ilkd.key.java.declaration.ArrayDeclaration

All Implemented Interfaces:

ArrayType, ClassType, ClassTypeContainer, Member, ProgramModelElement, Type, Declaration, MemberDeclaration, TypeDeclarationContainer, ModelElement, NamedModelElement, NamedProgramElement, NonTerminalProgramElement, ProgramElement, ScopeDefiningElement, SourceElement, TypeScope, VariableScope, SVSubstitute

public class ArrayDeclaration
extends TypeDeclaration
implements ArrayType

KeY used to model arrays using only the ArrayType. As the only attribute of an array has been the length attribute, it has been handled in a different way than members of usual classes. As we need some implicit fields for array creation and initialisation, the special handling of arrays is not any longer practicable. So, this class introduce a 'virtual' declaration for array types containing all required members. Please not the array fields accessed by an index are not included, so arrays of different lengths with same base type belong to the same array declaration. Attention: In contrast to the other type declaration, array declarations may be added at runtime.

Field Summary

Fields

Modifier and Type	Field and Description
private java.lang.String	altNameRepresentation
private TypeReference	basetype reference to the type the elements of this array must subclass
private int	dim dimension of the array
private KeYJavaType	superType

Fields inherited from class de.uka.ilkd.key.java.declaration.TypeDeclaration

fullName, isLibrary, members, name, parentIsInterfaceDeclaration

Fields inherited from class de.uka.ilkd.key.java.declaration.JavaDeclaration

modArray

Constructor Summary

Constructors

Modifier	Constructor and Description
	ArrayDeclaration(ExtList children, TypeReference baseType, KeYJavaType superType) ArrayDeclaration
private	ArrayDeclaration(ExtList children, TypeReference baseType, ProgramElementName name, KeYJavaType superType)

Method Summary

Modifier and Type	Method and Description
private static ExtList	addLength(ExtList children, KeYJavaType superType)
static ProgramElementName	createName(TypeReference basetype)
private int	dimension() computes the dimension of this array
java.lang.String	getAlternativeNameRepresentation() full name of the array in alternative form, i.e.
TypeReference	getBaseType() Get the element/base type.
ProgramElement	getChildAt(int index) Returns the child at the specified index in this node's "virtual" child array
int	getChildCount() Returns the number of children of this node.
Literal	getDefaultValue() returns the default value of the given type according to JLS Sect. 4.5.5
int	getDimension() return the dimension of this array
ImmutableList<KeYJavaType>	getSupertypes() returns the local declared supertypes
boolean	isInterface() Arrays are never interfaces (but may have interface types as element types)
boolean	isStrictFp() Arrays are never strictfp.
boolean	isTransient() Arrays are never transient.
boolean	isVolatile() Arrays are never volatile.
FieldDeclaration	length()
void	prettyPrint(PrettyPrinter p) pretty prints an array declaration
java.lang.String	toString() toString
void	visit(Visitor v) calls the corresponding method of a visitor in order to perform some action/transformation on this element

Methods inherited from class de.uka.ilkd.key.java.declaration.TypeDeclaration

equals, getAllFields, getAllMethods, getAllSupertypes, getAllTypes, getConstructors, getFields, getFirstElement, getFullName, getLastElement, getMembers, getMethods, getName, getPackage, getProgramElementName, getTypeDeclarationAt, getTypeDeclarationCount, getTypes, isAbstract, isFinal, isLibraryClass, isPrivate, isProtected, isPublic, isStatic

Methods inherited from class de.uka.ilkd.key.java.declaration.JavaDeclaration

getModifiers, getStateCount, getVisibilityModifier, isGhost, isModel, isNative, isSynchronized

Methods inherited from class de.uka.ilkd.key.java.JavaNonTerminalProgramElement

compatibleBlockSize, computeHashCode, equalsModRenaming, getArrayPos, match, matchChildren

Methods inherited from class de.uka.ilkd.key.java.JavaProgramElement

getComments, hashCode, prettyPrintMain, reuseSignature

Methods inherited from class de.uka.ilkd.key.java.JavaSourceElement

getEndPosition, getFirstElementIncludingBlocks, getParentClass, getPositionInfo, getRelativePosition, getStartPosition, setParentClass, toSource, toString

Methods inherited from class java.lang.Object

clone, finalize, getClass, notify, notifyAll, wait, wait, wait

Methods inherited from interface de.uka.ilkd.key.java.abstraction.ArrayType

getFullName, getName

Methods inherited from interface de.uka.ilkd.key.java.Declaration

getModifiers

Methods inherited from interface de.uka.ilkd.key.java.ProgramElement

getComments, match

Methods inherited from interface de.uka.ilkd.key.java.SourceElement

equalsModRenaming, getEndPosition, getFirstElementIncludingBlocks, getPositionInfo, getRelativePosition, getStartPosition

Field Detail

basetype

private final TypeReference basetype

reference to the type the elements of this array must subclass

dim

private final int dim

dimension of the array

superType

private final KeYJavaType superType

altNameRepresentation

private java.lang.String altNameRepresentation

Constructor Detail

ArrayDeclaration

private ArrayDeclaration(ExtList children,
                         TypeReference baseType,
                         ProgramElementName name,
                         KeYJavaType superType)

ArrayDeclaration

public ArrayDeclaration(ExtList children,
                        TypeReference baseType,
                        KeYJavaType superType)

ArrayDeclaration

Parameters:

children - an ExtList with the basetype and member declarations of this type

Method Detail

addLength

private static ExtList addLength(ExtList children,
                                 KeYJavaType superType)

getChildCount

public int getChildCount()

Returns the number of children of this node.

Specified by:

getChildCount in interface NonTerminalProgramElement

Returns:

an int giving the number of children of this node

length

public FieldDeclaration length()

getChildAt

public ProgramElement getChildAt(int index)

Returns the child at the specified index in this node's "virtual" child array

Specified by:

getChildAt in interface NonTerminalProgramElement

Parameters:

index - an index into this node's "virtual" child array

Returns:

the program element at the given position

Throws:

java.lang.ArrayIndexOutOfBoundsException - if index is out of bounds

getBaseType

public TypeReference getBaseType()

Get the element/base type.

Specified by:

getBaseType in interface ArrayType

Returns:

refernce to the base type .

isStrictFp

public boolean isStrictFp()

Arrays are never strictfp.

Specified by:

isStrictFp in interface Member

Specified by:

isStrictFp in interface MemberDeclaration

Overrides:

isStrictFp in class TypeDeclaration

Returns:

true if this member is strictfp, false otherwise.

isTransient

public boolean isTransient()

Arrays are never transient.

Overrides:

isTransient in class JavaDeclaration

isVolatile

public boolean isVolatile()

Arrays are never volatile.

Overrides:

isVolatile in class JavaDeclaration

isInterface

public boolean isInterface()

Arrays are never interfaces (but may have interface types as element types)

Specified by:

isInterface in interface ClassType

Returns:

true if this object represents an interface, false if it is an ordinary class.

getDimension

public int getDimension()

return the dimension of this array

Specified by:

getDimension in interface ArrayType

Returns:

an int containing the array's dimension

getDefaultValue

public Literal getDefaultValue()

returns the default value of the given type according to JLS Sect. 4.5.5

Specified by:

getDefaultValue in interface Type

Overrides:

getDefaultValue in class TypeDeclaration

Returns:

the default value of the given type according to JLS Sect. 4.5.5

dimension

private int dimension()

computes the dimension of this array

createName

public static ProgramElementName createName(TypeReference basetype)

getAlternativeNameRepresentation

public java.lang.String getAlternativeNameRepresentation()

Description copied from interface: ArrayType

full name of the array in alternative form, i.e. e.g. int[] instead of [I

Specified by:

getAlternativeNameRepresentation in interface ArrayType

getSupertypes

public ImmutableList<KeYJavaType> getSupertypes()

returns the local declared supertypes

Specified by:

getSupertypes in interface ClassType

Specified by:

getSupertypes in class TypeDeclaration

Returns:

the array of locally defined supertypes of this type.

visit

public void visit(Visitor v)

calls the corresponding method of a visitor in order to perform some action/transformation on this element

Specified by:

visit in interface SourceElement

Parameters:

v - the Visitor

prettyPrint

public void prettyPrint(PrettyPrinter p)
                 throws java.io.IOException

pretty prints an array declaration

Specified by:

prettyPrint in interface SourceElement

Overrides:

prettyPrint in class JavaProgramElement

Parameters:

p - a pretty printer.

Throws:

java.io.IOException - occasionally thrown.

toString

public java.lang.String toString()

toString

Overrides:

toString in class JavaSourceElement