org.jmlspecs.jml4.esc.gc.lang.expr
Class CfgQuantifiedExpression

java.lang.Object
  org.jmlspecs.jml4.esc.gc.lang.expr.CfgExpression
      org.jmlspecs.jml4.esc.gc.lang.expr.CfgQuantifiedExpression

public class CfgQuantifiedExpression
extends CfgExpression

Field Summary

CfgExpression	body
CfgVarDecl[]	boundVariables
CfgQuantifier	quantifier
CfgExpression	range

Fields inherited from class org.jmlspecs.jml4.esc.gc.lang.expr.CfgExpression

sourceEnd, sourceStart, type

Constructor Summary

CfgQuantifiedExpression(CfgQuantifier quantifier, CfgExpression range, CfgExpression body, CfgVarDecl[] boundVariables, TypeBinding type, int sourceStart, int sourceEnd)

Method Summary

CfgExpression	accept(CfgExpressionVisitor visitor)
VC	accept(WlpVisitor visitor)
static CfgExpression	asBlock(CfgExpression body, CfgVarDecl[] boundVarDecls)
java.lang.String	toString()

Methods inherited from class java.lang.Object

equals, getClass, hashCode, notify, notifyAll, wait, wait, wait

Field Detail

quantifier

public final CfgQuantifier quantifier

range

public final CfgExpression range

body

public final CfgExpression body

boundVariables

public final CfgVarDecl[] boundVariables

Constructor Detail

CfgQuantifiedExpression

public CfgQuantifiedExpression(CfgQuantifier quantifier,
                               CfgExpression range,
                               CfgExpression body,
                               CfgVarDecl[] boundVariables,
                               TypeBinding type,
                               int sourceStart,
                               int sourceEnd)

Method Detail

accept

public VC accept(WlpVisitor visitor)

Specified by:

accept in class CfgExpression

accept

public CfgExpression accept(CfgExpressionVisitor visitor)

Specified by:

accept in class CfgExpression

toString

public java.lang.String toString()

Specified by:

toString in class CfgExpression

asBlock

public static CfgExpression asBlock(CfgExpression body,
                                    CfgVarDecl[] boundVarDecls)