org.jmlspecs.jml4.fspv.theory
Class TheoryVariable

java.lang.Object
  org.jmlspecs.jml4.fspv.theory.TheoryVariable

public class TheoryVariable
extends java.lang.Object

Field Summary

static int	ARGUMENT
static int	BOUND
int	declSourceStart
TheoryExpression	initialization
int	kind
static int	LOCAL
java.lang.String	name
static int	OLD
static java.lang.String	OLD_SUFFIX
static int	RESULT
static java.lang.String	RESULT_NAME
TheoryType	type

Constructor Summary

TheoryVariable(java.lang.String name, TheoryType type2, TheoryExpression initialization, int kind, int declSourceStart)

Method Summary

static TheoryVariable	Argument(java.lang.String name, TheoryType type, int declSourceStart)
static TheoryVariable	Bound(java.lang.String name, TheoryType type, TheoryExpression initialization, int declSourceStart)
boolean	equals(TheoryVariable v)
int	getDeclSourceStart()
java.lang.String	getDecoratedName()
TheoryType	getType()
boolean	isArgument()
boolean	isBound()
boolean	isLocal()
boolean	isOld()
boolean	isResult()
static TheoryVariable	Local(java.lang.String name, TheoryType type, TheoryExpression initialization, int declSourceStart)
TheoryVariableReference	nameReference()
static TheoryVariable	Old(TheoryVariable v)
static TheoryVariable	Result(TheoryType type)
java.lang.String	toString()
java.lang.Object	visit(TheoryVisitor visitor)

Methods inherited from class java.lang.Object

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

Field Detail

ARGUMENT

public static final int ARGUMENT

See Also:

Constant Field Values

RESULT

public static final int RESULT

See Also:

Constant Field Values

OLD

public static final int OLD

See Also:

Constant Field Values

LOCAL

public static final int LOCAL

See Also:

Constant Field Values

BOUND

public static final int BOUND

See Also:

Constant Field Values

OLD_SUFFIX

public static final java.lang.String OLD_SUFFIX

See Also:

Constant Field Values

RESULT_NAME

public static final java.lang.String RESULT_NAME

See Also:

Constant Field Values

name

public final java.lang.String name

type

public final TheoryType type

kind

public final int kind

initialization

public final TheoryExpression initialization

declSourceStart

public final int declSourceStart

Constructor Detail

TheoryVariable

public TheoryVariable(java.lang.String name,
                      TheoryType type2,
                      TheoryExpression initialization,
                      int kind,
                      int declSourceStart)

Method Detail

getDecoratedName

public java.lang.String getDecoratedName()

getType

public TheoryType getType()

getDeclSourceStart

public int getDeclSourceStart()

isArgument

public boolean isArgument()

isResult

public boolean isResult()

isOld

public boolean isOld()

isLocal

public boolean isLocal()

isBound

public boolean isBound()

nameReference

public TheoryVariableReference nameReference()

toString

public java.lang.String toString()

Overrides:

toString in class java.lang.Object

visit

public java.lang.Object visit(TheoryVisitor visitor)

Argument

public static TheoryVariable Argument(java.lang.String name,
                                      TheoryType type,
                                      int declSourceStart)

Result

public static TheoryVariable Result(TheoryType type)

Old

public static TheoryVariable Old(TheoryVariable v)

Local

public static TheoryVariable Local(java.lang.String name,
                                   TheoryType type,
                                   TheoryExpression initialization,
                                   int declSourceStart)

Bound

public static TheoryVariable Bound(java.lang.String name,
                                   TheoryType type,
                                   TheoryExpression initialization,
                                   int declSourceStart)

equals

public boolean equals(TheoryVariable v)