de.uka.ilkd.key.java.declaration

Class FieldDeclaration

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

de.uka.ilkd.key.java.declaration.FieldDeclaration

All Implemented Interfaces:

Declaration, MemberDeclaration, ModelElement, NonTerminalProgramElement, ProgramElement, TypeReferenceContainer, SourceElement, SVSubstitute

public class FieldDeclaration
extends VariableDeclaration
implements MemberDeclaration

Field declaration. taken from COMPOST and changed to achieve an immutable structure

Field Summary

Fields

Modifier and Type	Field and Description
protected ImmutableArray<FieldSpecification>	fieldSpecs Field specs.

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

parentIsInterfaceDeclaration, typeReference

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

modArray

Constructor Summary

Constructors

Constructor and Description
FieldDeclaration(ExtList children, boolean parentIsInterfaceDeclaration) Field declaration.
FieldDeclaration(Modifier[] mods, TypeReference typeRef, FieldSpecification[] vars, boolean parentIsInterfaceDeclaration) Field 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.
ImmutableArray<FieldSpecification>	getFieldSpecifications()
ImmutableArray<? extends VariableSpecification>	getVariables() Get variables.
boolean	isFinal() Test whether the declaration is final.
boolean	isGhost() Test whether the declaration is ghost (the jml modifier is meant).
boolean	isModel() Test whether the declaration is model (the jml modifier is meant).
boolean	isPrivate() Test whether the declaration is private.
boolean	isProtected() Test whether the declaration is protected.
boolean	isPublic() Test whether the declaration is public.
boolean	isStatic() Test whether the declaration is static.
boolean	isStrictFp() Test whether the declaration is strict FP.
boolean	isTransient() Test whether the declaration is transient.
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.VariableDeclaration

getFirstElement, getFirstElementIncludingBlocks, getLastElement, getTypeReference, getTypeReferenceAt, getTypeReferenceCount, parentIsInterfaceDeclaration

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

getModifiers, getStateCount, getVisibilityModifier, isAbstract, isNative, isSynchronized, isVolatile

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

compatibleBlockSize, computeHashCode, equals, 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, 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.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, getFirstElement, getFirstElementIncludingBlocks, getLastElement, getPositionInfo, getRelativePosition, getStartPosition

Field Detail

fieldSpecs

protected final ImmutableArray<FieldSpecification> fieldSpecs

Field specs.

Constructor Detail

FieldDeclaration

public FieldDeclaration(Modifier[] mods,
                        TypeReference typeRef,
                        FieldSpecification[] vars,
                        boolean parentIsInterfaceDeclaration)

Field declaration.

Parameters:

mods - a modifier mutable list.

typeRef - a type reference.

vars - a variable specification array.

parentIsInterfaceDeclaration - a boolean set true iff parent is an InterfaceDeclaration

FieldDeclaration

public FieldDeclaration(ExtList children,
                        boolean parentIsInterfaceDeclaration)

Field declaration.

Parameters:

children - an ExtList of children. May include: several FieldSpecification (for the field) a TypeReference (as reference to the type of the declared variable) several Modifier (taken as modifiers of the declaration), a Comment

parentIsInterfaceDeclaration - a boolean set true

Method Detail

getFieldSpecifications

public ImmutableArray<FieldSpecification> getFieldSpecifications()

getVariables

public ImmutableArray<? extends VariableSpecification> getVariables()

Description copied from class: VariableDeclaration

Get variables.

Specified by:

getVariables in class VariableDeclaration

Returns:

the variable specification array wrapper

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

isFinal

public boolean isFinal()

Test whether the declaration is final. Fields of interfaces are always final.

Overrides:

isFinal in class VariableDeclaration

isPrivate

public boolean isPrivate()

Test whether the declaration is private.

Specified by:

isPrivate in interface MemberDeclaration

Overrides:

isPrivate in class JavaDeclaration

isProtected

public boolean isProtected()

Test whether the declaration is protected.

Specified by:

isProtected in interface MemberDeclaration

Overrides:

isProtected in class JavaDeclaration

isPublic

public boolean isPublic()

Test whether the declaration is public. Fields of interfaces are always public.

Specified by:

isPublic in interface MemberDeclaration

Overrides:

isPublic in class JavaDeclaration

isStatic

public boolean isStatic()

Description copied from class: JavaDeclaration

Test whether the declaration is static.

Specified by:

isStatic in interface MemberDeclaration

Overrides:

isStatic in class JavaDeclaration

isTransient

public boolean isTransient()

Test whether the declaration is transient.

Overrides:

isTransient in class JavaDeclaration

isStrictFp

public boolean isStrictFp()

Test whether the declaration is strict FP.

Specified by:

isStrictFp in interface MemberDeclaration

Overrides:

isStrictFp in class JavaDeclaration

isModel

public boolean isModel()

Test whether the declaration is model (the jml modifier is meant).

Overrides:

isModel in class JavaDeclaration

isGhost

public boolean isGhost()

Test whether the declaration is ghost (the jml modifier is meant).

Overrides:

isGhost in class JavaDeclaration

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

Overrides:

visit in class VariableDeclaration

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 VariableDeclaration

Parameters:

p - a pretty printer.

Throws:

java.io.IOException - occasionally thrown.