| java.lang.Object
 de.uka.ilkd.key.logic.op.TermSymbol
de.uka.ilkd.key.logic.op.Function
de.uka.ilkd.key.logic.op.NonRigidFunction
de.uka.ilkd.key.logic.op.ProgramMethod
| getAnnotationCount | | public int getAnnotationCount()(Code) | | |
| getChildCount | | public int getChildCount()(Code) | | |
| getEndPosition | | public Position getEndPosition()(Code) | | 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().
the end position of the primary token. |
| getModifiers | | public ArrayOfModifier getModifiers()(Code) | | |
| getParameterDeclarationCount | | public int getParameterDeclarationCount()(Code) | | |
| getParameterType | | public KeYJavaType getParameterType(int i)(Code) | | returns the KeYJavaType of the i-th paramter declaration. This method
does not care about the invoker as argSort does.
Parameters:
i - the int specifying the parameter position the KeYJavaType of the i-th parameter |
| getParameters | | public ArrayOfParameterDeclaration getParameters()(Code) | | |
| getRelativePosition | | public Position getRelativePosition()(Code) | | 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().
the relative position of the primary token. |
| getStartPosition | | public Position getStartPosition()(Code) | | 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().
the start position of the primary token. |
| getVariableSpecification | | public VariableSpecification getVariableSpecification(int index)(Code) | | returns the variablespecification of the i-th parameterdeclaration
|
| isAbstract | | public boolean isAbstract()(Code) | | |
| isConstructor | | public boolean isConstructor()(Code) | | Test whether the declaration is a constructor.
|
| isFinal | | public boolean isFinal()(Code) | | |
| isImplicit | | public boolean isImplicit()(Code) | | |
| isModel | | public boolean isModel()(Code) | | Test whether the declaration is model.
|
| isNative | | public boolean isNative()(Code) | | |
| isPrivate | | public boolean isPrivate()(Code) | | Test whether the declaration is private.
|
| isProtected | | public boolean isProtected()(Code) | | Test whether the declaration is protected.
|
| isPublic | | public boolean isPublic()(Code) | | Test whether the declaration is public.
|
| isStatic | | public boolean isStatic()(Code) | | Test whether the declaration is static.
|
| isStrictFp | | public boolean isStrictFp()(Code) | | Test whether the declaration is strictfp.
|
| isSynchronized | | public boolean isSynchronized()(Code) | | |
| validTopLevel | | public boolean validTopLevel(Term term)(Code) | | BUG: remove this method bit first adopt the jml translation to take about the
correct type of parameters and automatic type conversion
true iff number of subterms of term is equal to its own arity |
| visit | | public void visit(Visitor v)(Code) | | calls the corresponding method of a visitor in order to
perform some action/transformation on this element
Parameters:
v - the Visitor |
|
|