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

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

All Implemented Interfaces:

java.lang.Comparable

public class VcRelativeExpression
extends VcBinaryExpression

Field Summary

VcOperator

operator

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

left, right

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

EMPTY, NEGLBL, NO_LBL, sourceEnd, sourceStart, type

Constructor Summary

VcRelativeExpression(VcOperator operator, VC left, VC right, int sourceStart, int sourceEnd)

VcRelativeExpression(VcOperator operator, VC left, VC right, KindOfAssertion kindOfAssertion, int kindOfLabel, int sourceStart, int sourceEnd, int labelStart)

Method Summary

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

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

getVarDecls

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

operator

public final VcOperator operator

Constructor Detail

VcRelativeExpression

public VcRelativeExpression(VcOperator operator,
                            VC left,
                            VC right,
                            KindOfAssertion kindOfAssertion,
                            int kindOfLabel,
                            int sourceStart,
                            int sourceEnd,
                            int labelStart)

VcRelativeExpression

public VcRelativeExpression(VcOperator operator,
                            VC left,
                            VC right,
                            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

hashCode

public int hashCode()

Specified by:

hashCode in class VC