org.jmlspecs.jml4.ast
Class JmlQuantifier

java.lang.Object
  org.jmlspecs.jml4.ast.JmlQuantifier

Direct Known Subclasses:

JmlBooleanQuantifier, JmlNumericQuantifier

public abstract class JmlQuantifier
extends java.lang.Object

Field Summary

static java.lang.String	EXISTS The \exists quantifier lexeme.
static java.lang.String	FORALL The \forall quantifier lexeme.
java.lang.String	lexeme The lexeme of this quantifier.
static java.lang.String	MAX The \max quantifier lexeme.
static java.lang.String	MIN The \min quantifier lexeme.
static java.lang.String	NUM_OF The \num_of quantifier lexeme.
static java.lang.String	PRODUCT The \product quantifier lexeme.
static java.lang.String	SUM The \sum quantifier lexeme.
TypeBinding	type The type of this quantifier (null means the type of the body).

Method Summary

static JmlQuantifier	fromLexeme(java.lang.String lexeme) Factory method for obtaining quantifiers from quantifier lexemes.
abstract void	generateCode(LocalDeclaration[] boundVariables, Expression range, Expression body, BlockScope currentScope, CodeStream codeStream, boolean valueRequired) Generates code for this quantifier.
TypeBinding	getFirstLegalType()
boolean	isLegalType(TypeBinding queryType)

Methods inherited from class java.lang.Object

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

Field Detail

FORALL

public static final java.lang.String FORALL

The \forall quantifier lexeme.

See Also:

Constant Field Values

EXISTS

public static final java.lang.String EXISTS

The \exists quantifier lexeme.

See Also:

Constant Field Values

NUM_OF

public static final java.lang.String NUM_OF

The \num_of quantifier lexeme.

See Also:

Constant Field Values

MAX

public static final java.lang.String MAX

The \max quantifier lexeme.

See Also:

Constant Field Values

MIN

public static final java.lang.String MIN

The \min quantifier lexeme.

See Also:

Constant Field Values

PRODUCT

public static final java.lang.String PRODUCT

The \product quantifier lexeme.

See Also:

Constant Field Values

SUM

public static final java.lang.String SUM

The \sum quantifier lexeme.

See Also:

Constant Field Values

lexeme

public final java.lang.String lexeme

The lexeme of this quantifier.

type

public final TypeBinding type

The type of this quantifier (null means the type of the body).

Method Detail

isLegalType

public boolean isLegalType(TypeBinding queryType)

Returns:

true if the specified type is legal for the body of this quantifier, false otherwise.

getFirstLegalType

public TypeBinding getFirstLegalType()

Returns:

the first legal type in the legal type array (for reporting purposes).

generateCode

public abstract void generateCode(LocalDeclaration[] boundVariables,
                                  Expression range,
                                  Expression body,
                                  BlockScope currentScope,
                                  CodeStream codeStream,
                                  boolean valueRequired)

Generates code for this quantifier. Currently unimplemented, and likely to be implemented only in child classes.

Parameters:

boundVariables - The bound variables.

range - The range.

body - The body.

currentScope - The current scope.

codeStream - The code stream.

valueRequired - The value required flag.

fromLexeme

public static JmlQuantifier fromLexeme(java.lang.String lexeme)

Factory method for obtaining quantifiers from quantifier lexemes.

Parameters:

lexeme - The lexeme.

Returns:

the appropriate quantifier for the specified lexeme, or null if no such quantifier exists.