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

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

All Implemented Interfaces:

java.lang.Comparable

public class VcQuantifiedExpression
extends VC

Field Summary

VC	body
boolean	isBlock
VcQuantifier	quantifier
VC	range

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

EMPTY, NEGLBL, NO_LBL, sourceEnd, sourceStart, type

Constructor Summary

VcQuantifiedExpression(VcQuantifier quantifier, VcVarDecl[] boundVarDecls, VC body)

VcQuantifiedExpression(VcQuantifier quantifier, VC range, VC body, TypeBinding type, int sourceStart, int sourceEnd)

VcQuantifiedExpression(VcQuantifier quantifier, VC range, VC body, 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)
VcVarDecl[]	boundVarDecls()
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

quantifier

public final VcQuantifier quantifier

range

public final VC range

body

public final VC body

isBlock

public final boolean isBlock

Constructor Detail

VcQuantifiedExpression

public VcQuantifiedExpression(VcQuantifier quantifier,
                              VC range,
                              VC body,
                              TypeBinding type,
                              KindOfAssertion kindOfAssertion,
                              int kindOfLabel,
                              int sourceStart,
                              int sourceEnd,
                              int labelStart)

VcQuantifiedExpression

public VcQuantifiedExpression(VcQuantifier quantifier,
                              VC range,
                              VC body,
                              TypeBinding type,
                              int sourceStart,
                              int sourceEnd)

VcQuantifiedExpression

public VcQuantifiedExpression(VcQuantifier quantifier,
                              VcVarDecl[] boundVarDecls,
                              VC body)

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

hashCode

public int hashCode()

Specified by:

hashCode in class VC

toString

public java.lang.String toString()

Specified by:

toString in class VC

boundVarDecls

public VcVarDecl[] boundVarDecls()