org.jmlspecs.jml4.fspv.theory.ast
Class TheoryMethodDeclaration

java.lang.Object
  org.jmlspecs.jml4.fspv.theory.ast.TheoryNode
      org.jmlspecs.jml4.fspv.theory.ast.TheoryMethodDeclaration

Direct Known Subclasses:

TheoryConstructorDeclaration

public class TheoryMethodDeclaration
extends TheoryNode

Field Summary

TheoryArgument[]	arguments
TheoryLocalDeclaration[]	locals
TheoryExpression	postcondition
TheoryExpression	precondition
TheoryStatement[]	statements

Fields inherited from class org.jmlspecs.jml4.fspv.theory.ast.TheoryNode

base, enclosingTheory

Constructor Summary

TheoryMethodDeclaration(ASTNode base, Theory theory, TheoryExpression pre, TheoryExpression post, TheoryArgument[] arguments, TheoryLocalDeclaration[] locals, TheoryStatement[] statements)

Method Summary

java.lang.String	getEnclosingType()
java.lang.String	getName()
boolean	hasLocals()
boolean	isReturnTypeBool()
boolean	isReturnTypeInt()
boolean	isReturnTypeNat()
boolean	isReturnTypeRef()
boolean	isReturnTypeVoid()
boolean	isStatic()
void	traverse(TheoryVisitor visitor)

Methods inherited from class org.jmlspecs.jml4.fspv.theory.ast.TheoryNode

toString

Methods inherited from class java.lang.Object

equals, getClass, hashCode, notify, notifyAll, wait, wait, wait

Field Detail

precondition

public final TheoryExpression precondition

postcondition

public final TheoryExpression postcondition

arguments

public final TheoryArgument[] arguments

locals

public final TheoryLocalDeclaration[] locals

statements

public final TheoryStatement[] statements

Constructor Detail

TheoryMethodDeclaration

public TheoryMethodDeclaration(ASTNode base,
                               Theory theory,
                               TheoryExpression pre,
                               TheoryExpression post,
                               TheoryArgument[] arguments,
                               TheoryLocalDeclaration[] locals,
                               TheoryStatement[] statements)

Method Detail

hasLocals

public boolean hasLocals()

getEnclosingType

public java.lang.String getEnclosingType()

getName

public java.lang.String getName()

isStatic

public boolean isStatic()

traverse

public void traverse(TheoryVisitor visitor)

Specified by:

traverse in class TheoryNode

isReturnTypeVoid

public boolean isReturnTypeVoid()

isReturnTypeInt

public boolean isReturnTypeInt()

isReturnTypeNat

public boolean isReturnTypeNat()

isReturnTypeBool

public boolean isReturnTypeBool()

isReturnTypeRef

public boolean isReturnTypeRef()