de.uka.ilkd.key.java.declaration

Class ClassDeclaration

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.ClassDeclaration

All Implemented Interfaces:

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

Direct Known Subclasses:

EnumClassDeclaration

public class ClassDeclaration
extends TypeDeclaration
implements Statement

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.
Binary classes may have only binary members. taken from COMPOST and changed to achieve an immutable structure

Field Summary

Fields

Modifier and Type	Field and Description
protected Extends	extending
protected Implements	implementing
protected boolean	isAnonymousClass
protected boolean	isInnerClass
protected boolean	isLocalClass

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

Constructor and Description
ClassDeclaration(ExtList children, ProgramElementName fullName, boolean isLibrary)
ClassDeclaration(ExtList children, ProgramElementName fullName, boolean isLibrary, boolean innerClass, boolean anonymousClass, boolean localClass) uses children list to create non-anonymous class
ClassDeclaration(Modifier[] mods, ProgramElementName name, Extends extended, ProgramElementName fullName, Implements implemented, MemberDeclaration[] members, boolean parentIsInterfaceDeclaration, boolean isLibrary) Class declaration.

Method Summary

Modifier and Type	Method and Description
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.
Extends	getExtendedTypes() Get extended types.
Implements	getImplementedTypes() Get implemented types.
ImmutableList<KeYJavaType>	getSupertypes() returns the local declared supertypes
boolean	isAnonymousClass()
boolean	isInnerClass()
boolean	isInterface() Checks if this class type denotes an interface.
boolean	isLocalClass()
boolean	isStrictFp() Classes are never strictfp.
boolean	isTransient() Classes are never transient.
boolean	isVolatile() Classes are never volatile.
void	prettyPrint(PrettyPrinter p) Pretty printing the source element.
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, getDefaultValue, 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, 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.ProgramElement

getComments, match

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

equalsModRenaming, getEndPosition, getFirstElement, getFirstElementIncludingBlocks, getLastElement, getPositionInfo, getRelativePosition, getStartPosition

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

getModifiers

Field Detail

extending

protected final Extends extending

implementing

protected final Implements implementing

isInnerClass

protected final boolean isInnerClass

isLocalClass

protected final boolean isLocalClass

isAnonymousClass

protected final boolean isAnonymousClass

Constructor Detail

ClassDeclaration

public ClassDeclaration(Modifier[] mods,
                        ProgramElementName name,
                        Extends extended,
                        ProgramElementName fullName,
                        Implements implemented,
                        MemberDeclaration[] members,
                        boolean parentIsInterfaceDeclaration,
                        boolean isLibrary)

Class declaration.

Parameters:

mods - a modifier array.

name - Identifier of the class

members - an array containing the memberdeclarations of this type

implemented - of type Implement containing the interfaces implemented by this class

extended - Extend containing the class extended by the class of this classdeclaration

parentIsInterfaceDeclaration - boolean true iff parent is an InterfaceDeclaration

ClassDeclaration

public ClassDeclaration(ExtList children,
                        ProgramElementName fullName,
                        boolean isLibrary,
                        boolean innerClass,
                        boolean anonymousClass,
                        boolean localClass)

uses children list to create non-anonymous class

Parameters:

children - the ExtList with all children building up this class declaration May contain: a Extends (as pointer to a class), a Implements (as pointer to an interface) ProgramElementName (as name), several MemberDeclaration (as members of the type), a parentIsInterfaceDeclaration (indicating if parent is interface), several Modifier (as modifiers of the type decl), a Comment

fullName - the fully qualified ProgramElementName of this class

isLibrary - a boolean flag indicating if this class represents a library class (such classes have usually no method implementations but specifications)

ClassDeclaration

public ClassDeclaration(ExtList children,
                        ProgramElementName fullName,
                        boolean isLibrary)

Method Detail

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

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

getExtendedTypes

public Extends getExtendedTypes()

Get extended types.

Returns:

the extends.

getImplementedTypes

public Implements getImplementedTypes()

Get implemented types.

Returns:

the implements.

isStrictFp

public boolean isStrictFp()

Classes 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()

Classes are never transient.

Overrides:

isTransient in class JavaDeclaration

isInnerClass

public boolean isInnerClass()

isAnonymousClass

public boolean isAnonymousClass()

isLocalClass

public boolean isLocalClass()

isVolatile

public boolean isVolatile()

Classes are never volatile.

Overrides:

isVolatile in class JavaDeclaration

isInterface

public boolean isInterface()

Description copied from interface: ClassType

Checks if this class type denotes an interface.

Specified by:

isInterface in interface ClassType

Returns:

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

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

Description copied from class: JavaSourceElement

Pretty printing the source element.

Specified by:

prettyPrint in interface SourceElement

Overrides:

prettyPrint in class JavaProgramElement

Parameters:

p - a pretty printer.

Throws:

java.io.IOException - occasionally thrown.