de.uka.ilkd.key.logic.op

Interface IProgramMethod

All Superinterfaces:

Declaration, IObserverFunction, MemberDeclaration, ModelElement, Named, NonTerminalProgramElement, Operator, ProgramElement, SortedOperator, SourceElement, SVSubstitute

All Known Subinterfaces:

ProgramConstruct

All Known Implementing Classes:

ProgramMethod, ProgramSV

public interface IProgramMethod
extends IObserverFunction, SourceElement, ProgramElement, MemberDeclaration

Method Summary

Modifier and Type	Method and Description
ImmutableList<LocationVariable>	collectParameters()
StatementBlock	getBody()
java.lang.String	getFullName()
MethodDeclaration	getMethodDeclaration()
java.lang.String	getName()
ParameterDeclaration	getParameterDeclarationAt(int index)
int	getParameterDeclarationCount()
ImmutableArray<ParameterDeclaration>	getParameters()
KeYJavaType	getParameterType(int i) returns the KeYJavaType of the i-th parameter declaration.
ImmutableArray<KeYJavaType>	getParamTypes() Returns the parameter types of this observer symbol.
ProgramElementName	getProgramElementName()
KeYJavaType	getReturnType()
Throws	getThrown()
java.lang.String	getUniqueName()
VariableSpecification	getVariableSpecification(int index) Returns the variablespecification of the i-th parameterdeclaration
boolean	isAbstract()
boolean	isConstructor() Test whether the declaration is a constructor.
boolean	isFinal()
boolean	isImplicit()
boolean	isModel() Test whether the declaration is model.
boolean	isNative()
boolean	isSynchronized()
boolean	isVoid()

Methods inherited from interface de.uka.ilkd.key.logic.op.IObserverFunction

getContainerType, getHeapCount, getNumParams, getParamType, getStateCount, getType, isStatic

Methods inherited from interface de.uka.ilkd.key.logic.op.SortedOperator

argSort, argSorts, sort

Methods inherited from interface de.uka.ilkd.key.logic.op.Operator

arity, bindVarsAt, isRigid, sort, validTopLevel

Methods inherited from interface de.uka.ilkd.key.logic.Named

name

Methods inherited from interface de.uka.ilkd.key.java.declaration.MemberDeclaration

isPrivate, isProtected, isPublic, isStatic, isStrictFp

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

getModifiers

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

getChildAt, getChildCount

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, prettyPrint, visit

Method Detail

getMethodDeclaration

MethodDeclaration getMethodDeclaration()

getParameterType

KeYJavaType getParameterType(int i)

returns the KeYJavaType of the i-th parameter declaration. This method does not care about the invoker as argSort does.

Parameters:

i - the int specifying the parameter position

Returns:

the KeYJavaType of the i-th parameter

getBody

StatementBlock getBody()

isConstructor

boolean isConstructor()

Test whether the declaration is a constructor.

isModel

boolean isModel()

Test whether the declaration is model.

isVoid

boolean isVoid()

getReturnType

KeYJavaType getReturnType()

Returns:

the return type

getProgramElementName

ProgramElementName getProgramElementName()

getUniqueName

java.lang.String getUniqueName()

getFullName

java.lang.String getFullName()

getName

java.lang.String getName()

isAbstract

boolean isAbstract()

isImplicit

boolean isImplicit()

isNative

boolean isNative()

isFinal

boolean isFinal()

isSynchronized

boolean isSynchronized()

getThrown

Throws getThrown()

getParameterDeclarationAt

ParameterDeclaration getParameterDeclarationAt(int index)

getVariableSpecification

VariableSpecification getVariableSpecification(int index)

Returns the variablespecification of the i-th parameterdeclaration

getParameterDeclarationCount

int getParameterDeclarationCount()

getParameters

ImmutableArray<ParameterDeclaration> getParameters()

getParamTypes

ImmutableArray<KeYJavaType> getParamTypes()

Description copied from interface: IObserverFunction

Returns the parameter types of this observer symbol. "Parameters" here includes only the *explicit* parameters, not the heap and the receiver object.

Specified by:

getParamTypes in interface IObserverFunction

collectParameters

ImmutableList<LocationVariable> collectParameters()

Returns:

The list of LocationVariables passed as parameters to this IProgramMethod.