org.jmlspecs.jml4.ast
Class JmlNumericQuantifier

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

public class JmlNumericQuantifier
extends JmlQuantifier

Field Summary

Fields inherited from class org.jmlspecs.jml4.ast.JmlQuantifier

EXISTS, FORALL, lexeme, MAX, MIN, NUM_OF, PRODUCT, SUM, type

Constructor Summary

JmlNumericQuantifier(java.lang.String lexeme, TypeBinding type, TypeBinding[] legalTypes)
Constructs a new JmlQuantifier with the specified properties.

Method Summary

void	generateCode(LocalDeclaration[] boundVariables, Expression range, Expression body, BlockScope currentScope, CodeStream codeStream, boolean valueRequired) Generates code for this quantifier; currently, this just puts the constant value 0 on the stack with an appropriate numeric type.
void	traverse(ASTVisitor visitor, BlockScope scope)

Methods inherited from class org.jmlspecs.jml4.ast.JmlQuantifier

fromLexeme, getFirstLegalType, isLegalType

Methods inherited from class java.lang.Object

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

Constructor Detail

JmlNumericQuantifier

public JmlNumericQuantifier(java.lang.String lexeme,
                            TypeBinding type,
                            TypeBinding[] legalTypes)

Constructs a new JmlQuantifier with the specified properties.

Parameters:

lexeme - The lexeme.

legalTypes - The legal body types.

Method Detail

generateCode

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

Generates code for this quantifier; currently, this just puts the constant value 0 on the stack with an appropriate numeric type.

Specified by:

generateCode in class JmlQuantifier

Parameters:

boundVariables - The bound variables.

range - The range.

body - The body.

currentScope - The current scope.

codeStream - The code stream.

valueRequired - The value required flag (unused here).

traverse

public void traverse(ASTVisitor visitor,
                     BlockScope scope)