org.jmlspecs.jml4.esc.vc.lang
Class VC

java.lang.Object
  org.jmlspecs.jml4.esc.vc.lang.VC

All Implemented Interfaces:

java.lang.Comparable

Direct Known Subclasses:

VcAndNary, VcArrayAllocationExpression, VcArrayReference, VcBinaryExpression, VcBooleanConstant, VcConditionalExpression, VcFieldReference, VcFieldStore, VcIntegerConstant, VcNot, VcQuantifiedExpression, VcThisReference, VcVarDecl, VcVariable

public abstract class VC
extends java.lang.Object
implements java.lang.Comparable

Field Summary

static VC[]	EMPTY
static int	NEGLBL
static int	NO_LBL
int	sourceEnd
int	sourceStart
TypeBinding	type

Constructor Summary

VC(TypeBinding type, int sourceStart, int sourceEnd)

VC(TypeBinding type, KindOfAssertion kindOfAssertion, int kindOfLabel, int sourceStart, int sourceEnd, int labelStart)

Method Summary

abstract java.lang.String	accept(ProverVisitor visitor)
java.lang.String	acceptAsTerm(ProverVisitor visitor)
void	addDecl(VcVarDecl decl)
void	addDecls(java.util.List newDecls)
int	compareTo(java.lang.Object o)
java.util.List	decls()
java.lang.String	declString()
boolean	endsInImpliesTrue()
boolean	equals(java.lang.Object obj)
java.lang.String	getName()
abstract int	hashCode()
boolean	hasName()
boolean	isImplication()
KindOfAssertion	kindOfAssertion()
int	kindOfLabel()
int	labelStart()
void	markAsImplication()
VC	negateLastImplication()
void	setLabel(KindOfAssertion kindOfAssertion, int kindOfLabel, int labelStart)
void	setName(java.lang.String name)
abstract java.lang.String	toString()
java.lang.String	toStringWithName()
java.lang.String	visitVarDecls(ProverVisitor visitor)

Methods inherited from class java.lang.Object

getClass, notify, notifyAll, wait, wait, wait

Field Detail

EMPTY

public static final VC[] EMPTY

type

public final TypeBinding type

sourceStart

public final int sourceStart

sourceEnd

public final int sourceEnd

NO_LBL

public static final int NO_LBL

See Also:

Constant Field Values

NEGLBL

public static final int NEGLBL

See Also:

Constant Field Values

Constructor Detail

VC

public VC(TypeBinding type,
          KindOfAssertion kindOfAssertion,
          int kindOfLabel,
          int sourceStart,
          int sourceEnd,
          int labelStart)

VC

public VC(TypeBinding type,
          int sourceStart,
          int sourceEnd)

Method Detail

setLabel

public void setLabel(KindOfAssertion kindOfAssertion,
                     int kindOfLabel,
                     int labelStart)

kindOfAssertion

public KindOfAssertion kindOfAssertion()

kindOfLabel

public int kindOfLabel()

labelStart

public int labelStart()

toString

public abstract java.lang.String toString()

Overrides:

toString in class java.lang.Object

toStringWithName

public java.lang.String toStringWithName()

accept

public abstract java.lang.String accept(ProverVisitor visitor)

acceptAsTerm

public java.lang.String acceptAsTerm(ProverVisitor visitor)

decls

public java.util.List decls()

addDecl

public void addDecl(VcVarDecl decl)

addDecls

public void addDecls(java.util.List newDecls)

visitVarDecls

public java.lang.String visitVarDecls(ProverVisitor visitor)

declString

public java.lang.String declString()

getName

public java.lang.String getName()

hasName

public boolean hasName()

setName

public void setName(java.lang.String name)

hashCode

public abstract int hashCode()

Overrides:

hashCode in class java.lang.Object

endsInImpliesTrue

public boolean endsInImpliesTrue()

compareTo

public int compareTo(java.lang.Object o)

Specified by:

compareTo in interface java.lang.Comparable

equals

public boolean equals(java.lang.Object obj)

Overrides:

equals in class java.lang.Object

negateLastImplication

public VC negateLastImplication()

markAsImplication

public void markAsImplication()

isImplication

public boolean isImplication()