de.uka.ilkd.key.java.declaration

Class MethodDeclaration

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

All Implemented Interfaces:

ClassTypeContainer, Member, Method, ProgramModelElement, Declaration, MemberDeclaration, ModelElement, NamedModelElement, NamedProgramElement, NonTerminalProgramElement, ParameterContainer, ProgramElement, TypeReferenceContainer, ScopeDefiningElement, SourceElement, StatementContainer, VariableScope, SVSubstitute

Direct Known Subclasses:

ConstructorDeclaration

public class MethodDeclaration
extends JavaDeclaration
implements MemberDeclaration, TypeReferenceContainer, NamedProgramElement, ParameterContainer, Method, VariableScope

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

Field Summary

Fields

Modifier and Type	Field and Description
protected StatementBlock	body
protected Throws	exceptions
protected ProgramElementName	name
protected ImmutableArray<ParameterDeclaration>	parameters
protected boolean	parentIsInterfaceDeclaration this field stores if parent is an InterfaceDeclaration because we will be unable to walk the tree upwards to check this
protected TypeReference	returnType
protected Comment[]	voidComments

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

modArray

Constructor Summary

Constructors

Constructor and Description
MethodDeclaration(ExtList children, boolean parentIsInterfaceDeclaration, Comment[] voidComments) Method declaration.
MethodDeclaration(Modifier[] modifiers, TypeReference returnType, ProgramElementName name, ImmutableArray<ParameterDeclaration> parameters, Throws exceptions, StatementBlock body, boolean parentIsInterfaceDeclaration) Method declaration.
MethodDeclaration(Modifier[] modifiers, TypeReference returnType, ProgramElementName name, ParameterDeclaration[] parameters, Throws exceptions, StatementBlock body, boolean parentIsInterfaceDeclaration) Method declaration.

Method Summary

Modifier and Type	Method and Description
StatementBlock	getBody()
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.
SourceElement	getFirstElement() Finds the source element that occurs first in the source.
java.lang.String	getFullName() Returns the maximal expanded name including all applicable qualifiers.
SourceElement	getLastElement() Finds the source element that occurs last in the source.
java.lang.String	getName() Return the name of the model element.
ParameterDeclaration	getParameterDeclarationAt(int index) Return the parameter declaration at the specified index in this node's "virtual" parameter declaration array.
int	getParameterDeclarationCount() Get the number of parameters in this container.
ImmutableArray<ParameterDeclaration>	getParameters()
ProgramElementName	getProgramElementName() Get identifier.
int	getStateCount() Get the state count of the declaration
Statement	getStatementAt(int index)
int	getStatementCount() Get the number of statements in this container.
Throws	getThrown()
TypeReference	getTypeReference() Get return type.
TypeReference	getTypeReferenceAt(int index)
int	getTypeReferenceCount() Get the number of type references in this container.
Comment[]	getVoidComments()
boolean	isAbstract() Test whether the declaration is abstract.
boolean	isFinal() Test whether the declaration is final.
boolean	isModel() Test whether the declaration is model (the jml modifier is meant).
boolean	isNative() Test whether the declaration is native.
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 strictfp.
boolean	isSynchronized() Test whether the declaration is synchronized.
boolean	isVarArgMethod() test whether the declaration is a method with a variable number of arguments (i.e. the ellipsis ...)
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.JavaDeclaration

getModifiers, getVisibilityModifier, isGhost, isTransient, 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, 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.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

returnType

protected final TypeReference returnType

voidComments

protected final Comment[] voidComments

name

protected final ProgramElementName name

parameters

protected final ImmutableArray<ParameterDeclaration> parameters

exceptions

protected final Throws exceptions

body

protected final StatementBlock body

parentIsInterfaceDeclaration

protected final boolean parentIsInterfaceDeclaration

this field stores if parent is an InterfaceDeclaration because we will be unable to walk the tree upwards to check this

Constructor Detail

MethodDeclaration

public MethodDeclaration(ExtList children,
                         boolean parentIsInterfaceDeclaration,
                         Comment[] voidComments)

Method declaration.

Parameters:

children - an ExtList of children. May include: a TypeReference (as a reference to the return type), a de.uka.ilkd.key.logic.ProgramElementName (as Name of the method), several ParameterDeclaration (as parameters of the declared method), a StatementBlock (as body of the declared method), several Modifier (taken as modifiers of the declaration), a Comment

parentIsInterfaceDeclaration - a boolean set true iff parent is an InterfaceDeclaration

MethodDeclaration

public MethodDeclaration(Modifier[] modifiers,
                         TypeReference returnType,
                         ProgramElementName name,
                         ParameterDeclaration[] parameters,
                         Throws exceptions,
                         StatementBlock body,
                         boolean parentIsInterfaceDeclaration)

Method declaration.

Parameters:

modifiers - a modifier array

returnType - a type reference.

name - an identifier.

parameters - a parameter declaration mutable list.

exceptions - a throws.

body - a statement block.

parentIsInterfaceDeclaration - a boolean set true iff parent is an InterfaceDeclaration

MethodDeclaration

public MethodDeclaration(Modifier[] modifiers,
                         TypeReference returnType,
                         ProgramElementName name,
                         ImmutableArray<ParameterDeclaration> parameters,
                         Throws exceptions,
                         StatementBlock body,
                         boolean parentIsInterfaceDeclaration)

Method declaration.

Parameters:

modifiers - a modifier array

returnType - a type reference.

name - an identifier.

parameters - a parameter declaration mutable list.

exceptions - a throws.

body - a statement block.

parentIsInterfaceDeclaration - a boolean set true iff parent is an InterfaceDeclaration

Method Detail

getProgramElementName

public ProgramElementName getProgramElementName()

Description copied from interface: NamedProgramElement

Get identifier.

Specified by:

getProgramElementName in interface NamedProgramElement

Returns:

the identifier.

getFirstElement

public SourceElement getFirstElement()

Description copied from class: JavaSourceElement

Finds the source element that occurs first in the source. The default implementation returns this element, which is correct for all terminal program elements, and many non terminals such as statements and prefixed operators.

Specified by:

getFirstElement in interface SourceElement

Overrides:

getFirstElement in class JavaSourceElement

Returns:

the first source element in the syntactical representation of this element, may be equals to this element.

See Also:

JavaSourceElement.toSource(), JavaSourceElement.getStartPosition()

getLastElement

public SourceElement getLastElement()

Description copied from class: JavaSourceElement

Finds the source element that occurs last in the source. The default implementation returns this element, which is correct for all terminal program elements, and many non terminals such as statements and prefixed operators.

Specified by:

getLastElement in interface SourceElement

Overrides:

getLastElement in class JavaSourceElement

Returns:

the last source element in the syntactical representation of this element, may be equals to this element.

See Also:

JavaSourceElement.toSource(), JavaSourceElement.getEndPosition()

getChildCount

public int getChildCount()

Description copied from interface: NonTerminalProgramElement

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)

Description copied from interface: NonTerminalProgramElement

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

getStatementCount

public int getStatementCount()

Description copied from interface: StatementContainer

Get the number of statements in this container.

Specified by:

getStatementCount in interface StatementContainer

Returns:

the number of statements.

getStatementAt

public Statement getStatementAt(int index)

Specified by:

getStatementAt in interface StatementContainer

getTypeReferenceCount

public int getTypeReferenceCount()

Description copied from interface: TypeReferenceContainer

Get the number of type references in this container.

Specified by:

getTypeReferenceCount in interface TypeReferenceContainer

Returns:

the number of type references.

getTypeReferenceAt

public TypeReference getTypeReferenceAt(int index)

Specified by:

getTypeReferenceAt in interface TypeReferenceContainer

getParameterDeclarationCount

public int getParameterDeclarationCount()

Description copied from interface: ParameterContainer

Get the number of parameters in this container.

Specified by:

getParameterDeclarationCount in interface ParameterContainer

Returns:

the number of parameters.

getParameterDeclarationAt

public ParameterDeclaration getParameterDeclarationAt(int index)

Description copied from interface: ParameterContainer

Return the parameter declaration at the specified index in this node's "virtual" parameter declaration array.

Specified by:

getParameterDeclarationAt in interface ParameterContainer

Parameters:

index - an index for a parameter declaration.

Returns:

the parameter declaration with the given index.

getTypeReference

public TypeReference getTypeReference()

Get return type.

Returns:

the type reference.

getVoidComments

public Comment[] getVoidComments()

getName

public final java.lang.String getName()

Description copied from interface: NamedModelElement

Return the name of the model element.

Specified by:

getName in interface NamedModelElement

Returns:

the name of the model element.

getParameters

public ImmutableArray<ParameterDeclaration> getParameters()

getFullName

public java.lang.String getFullName()

Description copied from interface: ProgramModelElement

Returns the maximal expanded name including all applicable qualifiers.

Specified by:

getFullName in interface ProgramModelElement

Returns:

the full name of this program model element.

getThrown

public Throws getThrown()

getBody

public StatementBlock getBody()

isFinal

public boolean isFinal()

Description copied from class: JavaDeclaration

Test whether the declaration is final.

Specified by:

isFinal in interface Member

Overrides:

isFinal in class JavaDeclaration

Returns:

true if this member is final, false otherwise.

isPrivate

public boolean isPrivate()

Description copied from class: JavaDeclaration

Test whether the declaration is private.

Specified by:

isPrivate in interface Member

Specified by:

isPrivate in interface MemberDeclaration

Overrides:

isPrivate in class JavaDeclaration

Returns:

true if this member is private, false otherwise.

isProtected

public boolean isProtected()

Description copied from class: JavaDeclaration

Test whether the declaration is protected.

Specified by:

isProtected in interface Member

Specified by:

isProtected in interface MemberDeclaration

Overrides:

isProtected in class JavaDeclaration

Returns:

true if this member is protected, false otherwise.

isPublic

public boolean isPublic()

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

Specified by:

isPublic in interface Member

Specified by:

isPublic in interface MemberDeclaration

Overrides:

isPublic in class JavaDeclaration

Returns:

true if this member is public, false otherwise.

isStatic

public boolean isStatic()

Description copied from class: JavaDeclaration

Test whether the declaration is static.

Specified by:

isStatic in interface Member

Specified by:

isStatic in interface MemberDeclaration

Overrides:

isStatic in class JavaDeclaration

Returns:

true if this member is static, false otherwise.

isModel

public boolean isModel()

Description copied from class: JavaDeclaration

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

Overrides:

isModel in class JavaDeclaration

getStateCount

public int getStateCount()

Description copied from class: JavaDeclaration

Get the state count of the declaration

Overrides:

getStateCount in class JavaDeclaration

isVarArgMethod

public boolean isVarArgMethod()

test whether the declaration is a method with a variable number of arguments (i.e. the ellipsis ...)

Returns:

true iff so

isStrictFp

public boolean isStrictFp()

Description copied from class: JavaDeclaration

Test whether the declaration is strictfp.

Specified by:

isStrictFp in interface Member

Specified by:

isStrictFp in interface MemberDeclaration

Overrides:

isStrictFp in class JavaDeclaration

Returns:

true if this member is strictfp, false otherwise.

isAbstract

public boolean isAbstract()

Test whether the declaration is abstract. Methods of interfaces are always abstract.

Specified by:

isAbstract in interface Method

Overrides:

isAbstract in class JavaDeclaration

Returns:

true if this member is abstract, false otherwise.

See Also:

Constructor

isNative

public boolean isNative()

Test whether the declaration is native. Constructors are never native.

Specified by:

isNative in interface Method

Overrides:

isNative in class JavaDeclaration

Returns:

true if this method is native, false otherwise.

See Also:

Constructor

isSynchronized

public boolean isSynchronized()

Description copied from class: JavaDeclaration

Test whether the declaration is synchronized.

Specified by:

isSynchronized in interface Method

Overrides:

isSynchronized in class JavaDeclaration

Returns:

true if this method is synchronized, false otherwise.

See Also:

Constructor

visit

public void visit(Visitor v)

Description copied from interface: SourceElement

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.