org.jmlspecs.jml4.ast
Class JmlBooleanQuantifier

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

public class JmlBooleanQuantifier
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

JmlBooleanQuantifier(java.lang.String lexeme, 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 "true" on the stack.
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

JmlBooleanQuantifier

public JmlBooleanQuantifier(java.lang.String lexeme,
                            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 "true" on the stack.

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)