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

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

All Implemented Interfaces:

java.lang.Comparable

public final class VcBooleanConstant
extends VC

Field Summary

static VcBooleanConstant	TRUE
boolean	value

Fields inherited from class org.jmlspecs.jml4.esc.vc.lang.VC

EMPTY, NEGLBL, NO_LBL, sourceEnd, sourceStart, type

Constructor Summary

VcBooleanConstant(boolean value, int sourceStart, int sourceEnd)

VcBooleanConstant(boolean value, KindOfAssertion kindOfAssertion, int kindOfLabel, int sourceStart, int sourceEnd, int labelStart)

Method Summary

java.lang.String	accept(ProverVisitor visitor)
java.lang.String	acceptAsTerm(ProverVisitor visitor)
boolean	endsInImpliesTrue()
int	hashCode()
java.lang.String	toString()

Methods inherited from class org.jmlspecs.jml4.esc.vc.lang.VC

addDecl, addDecls, compareTo, decls, declString, equals, getName, hasName, isImplication, kindOfAssertion, kindOfLabel, labelStart, markAsImplication, negateLastImplication, setLabel, setName, toStringWithName, visitVarDecls

Methods inherited from class java.lang.Object

getClass, notify, notifyAll, wait, wait, wait

Field Detail

TRUE

public static final VcBooleanConstant TRUE

value

public final boolean value

Constructor Detail

VcBooleanConstant

public VcBooleanConstant(boolean value,
                         KindOfAssertion kindOfAssertion,
                         int kindOfLabel,
                         int sourceStart,
                         int sourceEnd,
                         int labelStart)

VcBooleanConstant

public VcBooleanConstant(boolean value,
                         int sourceStart,
                         int sourceEnd)

Method Detail

toString

public java.lang.String toString()

Specified by:

toString in class VC

accept

public java.lang.String accept(ProverVisitor visitor)

Specified by:

accept in class VC

acceptAsTerm

public java.lang.String acceptAsTerm(ProverVisitor visitor)

Overrides:

acceptAsTerm in class VC

hashCode

public int hashCode()

Specified by:

hashCode in class VC

endsInImpliesTrue

public boolean endsInImpliesTrue()

Overrides:

endsInImpliesTrue in class VC