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

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

All Implemented Interfaces:

java.lang.Comparable

public class VcConditionalExpression
extends VC

Field Summary

VC	condition
VC	valueIfFalse
VC	valueIfTrue

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

EMPTY, NEGLBL, NO_LBL, sourceEnd, sourceStart, type

Constructor Summary

VcConditionalExpression(VC condition, VC valueIfTrue, VC valueIfFalse, TypeBinding type, int sourceStart, int sourceEnd)

VcConditionalExpression(VC condition, VC valueIfTrue, VC valueIfFalse, TypeBinding type, KindOfAssertion kindOfAssertion, int kindOfLabel, int sourceStart, int sourceEnd, int labelStart)

Method Summary

java.lang.String	accept(ProverVisitor visitor)
java.lang.String	acceptAsTerm(ProverVisitor visitor)
java.util.List	getVarDecls()
int	hashCode()
java.lang.String	toString()

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

addDecl, addDecls, compareTo, decls, declString, endsInImpliesTrue, 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

condition

public final VC condition

valueIfTrue

public final VC valueIfTrue

valueIfFalse

public final VC valueIfFalse

Constructor Detail

VcConditionalExpression

public VcConditionalExpression(VC condition,
                               VC valueIfTrue,
                               VC valueIfFalse,
                               TypeBinding type,
                               KindOfAssertion kindOfAssertion,
                               int kindOfLabel,
                               int sourceStart,
                               int sourceEnd,
                               int labelStart)

VcConditionalExpression

public VcConditionalExpression(VC condition,
                               VC valueIfTrue,
                               VC valueIfFalse,
                               TypeBinding type,
                               int sourceStart,
                               int sourceEnd)

Method Detail

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

toString

public java.lang.String toString()

Specified by:

toString in class VC

getVarDecls

public java.util.List getVarDecls()

hashCode

public int hashCode()

Specified by:

hashCode in class VC