de.uka.ilkd.key.logic.op

Class ProgramMethod

java.lang.Object

de.uka.ilkd.key.logic.op.AbstractOperator

de.uka.ilkd.key.logic.op.AbstractSortedOperator

de.uka.ilkd.key.logic.op.Function

de.uka.ilkd.key.logic.op.ObserverFunction

de.uka.ilkd.key.logic.op.ProgramMethod

All Implemented Interfaces:

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

public final class ProgramMethod
extends ObserverFunction
implements ProgramInLogic, IProgramMethod

The program method represents a (pure) method in the logic. In case of a non-static method the first argument represents the object on which the method is invoked.

Field Summary

Fields

Modifier and Type	Field and Description
private MethodDeclaration	method
private PositionInfo	pi
private KeYJavaType	returnType Return type of the method.

Constructor Summary

Constructors

Constructor and Description
ProgramMethod(MethodDeclaration method, KeYJavaType container, KeYJavaType kjt, PositionInfo pi, Sort heapSort)
ProgramMethod(MethodDeclaration method, KeYJavaType container, KeYJavaType kjt, PositionInfo pi, Sort heapSort, int heapCount)

Method Summary

Modifier and Type	Method and Description
ImmutableList<LocationVariable>	collectParameters()
Expression	convertToProgram(Term t, ExtList l)
boolean	equalsModRenaming(SourceElement se, NameAbstractionTable nat) equals modulo renaming is described in class SourceElement.
StatementBlock	getBody()
ProgramElement	getChildAt(int i) Returns the child at the specified index in this node's "virtual" child array.
int	getChildCount() Returns the number of children of this node.
Comment[]	getComments() Get comments.
Position	getEndPosition() Returns the end position of the primary token of this element.
SourceElement	getFirstElement() Finds the source element that occurs first in the source.
SourceElement	getFirstElementIncludingBlocks() Finds the source element that occurs first in the source.
java.lang.String	getFullName()
KeYJavaType	getKJT() Deprecated.
SourceElement	getLastElement() Finds the source element that occurs last in the source.
MethodDeclaration	getMethodDeclaration()
ImmutableArray<Modifier>	getModifiers() Get the modifiers.
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.
private static ImmutableArray<KeYJavaType>	getParamTypes(MethodDeclaration md)
PositionInfo	getPositionInfo() complete position information
ProgramElementName	getProgramElementName()
Position	getRelativePosition() Returns the relative position (number of blank heading lines and columns) of the primary token of this element.
KeYJavaType	getReturnType()
Position	getStartPosition() Returns the start position of the primary token of this element.
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	isPrivate() Test whether the declaration is private.
boolean	isProtected() Test whether the declaration is protected.
boolean	isPublic() Test whether the declaration is public.
boolean	isStrictFp() Test whether the declaration is strictfp.
boolean	isSynchronized()
boolean	isVoid()
MatchConditions	match(SourceData source, MatchConditions matchCond) matches the source "text" (@link SourceData#getSource()) against the pattern represented by this object.
void	prettyPrint(PrettyPrinter w) Pretty print.
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.logic.op.ObserverFunction

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

Methods inherited from class de.uka.ilkd.key.logic.op.Function

isSkolemConstant, isUnique, proofToString, rename, toString

Methods inherited from class de.uka.ilkd.key.logic.op.AbstractSortedOperator

additionalValidTopLevel, additionalValidTopLevel2, argSort, argSorts, sort, sort

Methods inherited from class de.uka.ilkd.key.logic.op.AbstractOperator

arity, bindVarsAt, isRigid, name, validTopLevel, whereToBind

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

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

getParamTypes

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

isStatic

Field Detail

method

private final MethodDeclaration method

returnType

private final KeYJavaType returnType

Return type of the method. Must not be null. Use KeYJavaType.VOID_TYPE for void methods.

pi

private final PositionInfo pi

Constructor Detail

ProgramMethod

public ProgramMethod(MethodDeclaration method,
                     KeYJavaType container,
                     KeYJavaType kjt,
                     PositionInfo pi,
                     Sort heapSort)

ProgramMethod

public ProgramMethod(MethodDeclaration method,
                     KeYJavaType container,
                     KeYJavaType kjt,
                     PositionInfo pi,
                     Sort heapSort,
                     int heapCount)

Method Detail

getParamTypes

private static ImmutableArray<KeYJavaType> getParamTypes(MethodDeclaration md)

getMethodDeclaration

public MethodDeclaration getMethodDeclaration()

Specified by:

getMethodDeclaration in interface IProgramMethod

getParameterType

public KeYJavaType getParameterType(int i)

Description copied from interface: IProgramMethod

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

Specified by:

getParameterType in interface IProgramMethod

Parameters:

i - the int specifying the parameter position

Returns:

the KeYJavaType of the i-th parameter

getBody

public StatementBlock getBody()

Specified by:

getBody in interface IProgramMethod

getFirstElement

public SourceElement getFirstElement()

Description copied from interface: SourceElement

Finds the source element that occurs first in the source.

Specified by:

getFirstElement in interface SourceElement

Returns:

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

See Also:

SourceElement.getStartPosition()

getFirstElementIncludingBlocks

public SourceElement getFirstElementIncludingBlocks()

Description copied from interface: SourceElement

Finds the source element that occurs first in the source.

Specified by:

getFirstElementIncludingBlocks in interface SourceElement

Returns:

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

See Also:

SourceElement.getStartPosition()

getLastElement

public SourceElement getLastElement()

Description copied from interface: SourceElement

Finds the source element that occurs last in the source.

Specified by:

getLastElement in interface SourceElement

Returns:

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

See Also:

SourceElement.getEndPosition()

getComments

public Comment[] getComments()

Description copied from interface: ProgramElement

Get comments.

Specified by:

getComments in interface ProgramElement

Returns:

the comments.

prettyPrint

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

Description copied from interface: SourceElement

Pretty print.

Specified by:

prettyPrint in interface SourceElement

Parameters:

w - a pretty printer.

Throws:

java.io.IOException - occasionally thrown.

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

getStartPosition

public Position getStartPosition()

Returns the start position of the primary token of this element. To get the start position of the syntactical first token, call the corresponding method of getFirstElement().

Specified by:

getStartPosition in interface SourceElement

Returns:

the start position of the primary token.

getEndPosition

public Position getEndPosition()

Returns the end position of the primary token of this element. To get the end position of the syntactical first token, call the corresponding method of getLastElement().

Specified by:

getEndPosition in interface SourceElement

Returns:

the end position of the primary token.

getRelativePosition

public Position getRelativePosition()

Returns the relative position (number of blank heading lines and columns) of the primary token of this element. To get the relative position of the syntactical first token, call the corresponding method of getFirstElement().

Specified by:

getRelativePosition in interface SourceElement

Returns:

the relative position of the primary token.

getPositionInfo

public PositionInfo getPositionInfo()

Description copied from interface: SourceElement

complete position information

Specified by:

getPositionInfo in interface SourceElement

isPrivate

public boolean isPrivate()

Test whether the declaration is private.

Specified by:

isPrivate in interface MemberDeclaration

isProtected

public boolean isProtected()

Test whether the declaration is protected.

Specified by:

isProtected in interface MemberDeclaration

isPublic

public boolean isPublic()

Test whether the declaration is public.

Specified by:

isPublic in interface MemberDeclaration

isConstructor

public boolean isConstructor()

Description copied from interface: IProgramMethod

Test whether the declaration is a constructor.

Specified by:

isConstructor in interface IProgramMethod

isModel

public boolean isModel()

Description copied from interface: IProgramMethod

Test whether the declaration is model.

Specified by:

isModel in interface IProgramMethod

isStrictFp

public boolean isStrictFp()

Test whether the declaration is strictfp.

Specified by:

isStrictFp in interface MemberDeclaration

isVoid

public boolean isVoid()

Specified by:

isVoid in interface IProgramMethod

getModifiers

public ImmutableArray<Modifier> getModifiers()

Description copied from interface: Declaration

Get the modifiers.

Specified by:

getModifiers in interface Declaration

Returns:

the (original) list of modifiers wrapped .

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 i)

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:

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

Returns:

the program element at the given position

equalsModRenaming

public boolean equalsModRenaming(SourceElement se,
                                 NameAbstractionTable nat)

equals modulo renaming is described in class SourceElement.

Specified by:

equalsModRenaming in interface SourceElement

getKJT

@Deprecated
public KeYJavaType getKJT()

Deprecated.

getReturnType

public KeYJavaType getReturnType()

Specified by:

getReturnType in interface IProgramMethod

Returns:

the return type

convertToProgram

public Expression convertToProgram(Term t,
                                   ExtList l)

Specified by:

convertToProgram in interface ProgramInLogic

getProgramElementName

public ProgramElementName getProgramElementName()

Specified by:

getProgramElementName in interface IProgramMethod

getUniqueName

public java.lang.String getUniqueName()

Specified by:

getUniqueName in interface IProgramMethod

getFullName

public java.lang.String getFullName()

Specified by:

getFullName in interface IProgramMethod

getName

public java.lang.String getName()

Specified by:

getName in interface IProgramMethod

isAbstract

public boolean isAbstract()

Specified by:

isAbstract in interface IProgramMethod

isImplicit

public boolean isImplicit()

Specified by:

isImplicit in interface IProgramMethod

isNative

public boolean isNative()

Specified by:

isNative in interface IProgramMethod

isFinal

public boolean isFinal()

Specified by:

isFinal in interface IProgramMethod

isSynchronized

public boolean isSynchronized()

Specified by:

isSynchronized in interface IProgramMethod

getThrown

public Throws getThrown()

Specified by:

getThrown in interface IProgramMethod

getParameterDeclarationAt

public ParameterDeclaration getParameterDeclarationAt(int index)

Specified by:

getParameterDeclarationAt in interface IProgramMethod

getVariableSpecification

public VariableSpecification getVariableSpecification(int index)

Description copied from interface: IProgramMethod

Returns the variablespecification of the i-th parameterdeclaration

Specified by:

getVariableSpecification in interface IProgramMethod

getParameterDeclarationCount

public int getParameterDeclarationCount()

Specified by:

getParameterDeclarationCount in interface IProgramMethod

getParameters

public ImmutableArray<ParameterDeclaration> getParameters()

Specified by:

getParameters in interface IProgramMethod

match

public MatchConditions match(SourceData source,
                             MatchConditions matchCond)

Description copied from interface: ProgramElement

matches the source "text" (@link SourceData#getSource()) against the pattern represented by this object. In case of a successful match the resulting MatchConditions with the found instantiations of the schemavariables. If the match failed, null is returned instead.

Specified by:

match in interface ProgramElement

Parameters:

source - the SourceData with the program element to match

matchCond - the MatchConditions found up to this point

Returns:

the resulting match conditions or null if the match failed

collectParameters

public ImmutableList<LocationVariable> collectParameters()

Specified by:

collectParameters in interface IProgramMethod

Returns:

The list of LocationVariables passed as parameters to this IProgramMethod.