org.jmlspecs.jml4.rac.quantifiedexpression
Class QuantifiedExpressionTranslator

java.lang.Object
  org.jmlspecs.jml4.rac.quantifiedexpression.QuantifiedExpressionTranslator

public class QuantifiedExpressionTranslator
extends java.lang.Object

An abstract class for translating JML quantified expressions into Java source code. The translation rules for the JML universal/existential quantified expressions are defined as follows.

   [[(\forall T x; P; Q), r]] =
     Collection c = null;
     [[S, c]]  // S is the qset of P ==> Q
     r = c != null;
     if (r) {
        Iterator iter = c.iterator();
        for (r && iter.hasNext()) {
            T x = iter.next();
            [[P ==> Q, r]]
        }
     }
 

   [[(\exists T x; P; Q), r]] =
     Collection c = null;
     [[S, c]]  // S is the qset of P && Q
     r = c == null;
     if (!r) {
        Iterator iter = c.iterator();
        for (!r && iter.hasNext()) {
            T x = iter.next();
            [[P && Q, r]]
        }
     }
 

The translation rules for other quantifiers are defined in a similar way.

Version:

$Revision: 1.16 $

Author:

Yoonsik Cheon, Amritam Sarcar

Field Summary

PostStateExpressionTranslator

transExp translator for translating subexpressions

Constructor Summary

QuantifiedExpressionTranslator(VariableGenerator varGen, RacContext context, JmlQuantifiedExpression expr, java.lang.String resultVar, PostStateExpressionTranslator transExp, RacResult racResult, SourceTypeBinding typeBinding)
Constructs a new instance.

Method Summary

java.lang.String	generateLoop(ASTNode node) Tanslates a JML quantified expression into Java source code that, if executed, evaluates the given statement, node for each combination of bound variables of the quantified expression.
java.lang.String	getLocalBindings()
java.lang.String	getLocalVariables()
void	getLocalVariablesInQuantifiedExpression(java.lang.String evaluatorPUse) Fetches local variables in quantified expression.
void	setLocalBindings(java.lang.String str)
void	setLocalVariables(java.lang.String str)
java.lang.String	translate() Translates a JML quantified expression into Java source code and return the translated code.

Methods inherited from class java.lang.Object

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

Field Detail

transExp

public PostStateExpressionTranslator transExp

translator for translating subexpressions

Constructor Detail

QuantifiedExpressionTranslator

public QuantifiedExpressionTranslator(VariableGenerator varGen,
                                      RacContext context,
                                      JmlQuantifiedExpression expr,
                                      java.lang.String resultVar,
                                      PostStateExpressionTranslator transExp,
                                      RacResult racResult,
                                      SourceTypeBinding typeBinding)

Constructs a new instance.

Parameters:

varGen - variable generator to be used during translation to generate unique local variables.

expr - quantified expression to be translated.

resultVar - variable name to have the value of quantified expression in the translated code.

transExp - translator to use for translating subexpressions of the quantified expression.

racResult - data structure to store rac results

typeBinding - SourceType

Method Detail

translate

public java.lang.String translate()

Translates a JML quantified expression into Java source code and return the translated code. Refers to QuantifiedExpressionTranslator for the format of the generated code.

Returns:

translated Java source code.

Throws:

if - the quantified expression is not executable.

generateLoop

public java.lang.String generateLoop(ASTNode node)
                              throws NonExecutableQuantifierException

Tanslates a JML quantified expression into Java source code that, if executed, evaluates the given statement, node for each combination of bound variables of the quantified expression. For example, given a quantified expression

 (\forall int i; 
   i >= 0 && i < this.v.length; 
     this.v[i] >= \old(this.v[i]))
 

this method generates the following code:

 int i = 0;
 int l = this.v.length;
 while (i < l) {
   [[code for argument node]]
   i = i + 1;
 }
 

where l is a unique local variable generated by the runtime assertion checker compiler. This method is used in translating old expressions contained in quantified expressions.

Returns:

translated Java source code.

Throws:

if - the quantified expression is not executable.

NonExecutableQuantifierException

See Also:

TransPostcondition#visitJmlOldExpression(JmlOldExpression), TransPostcondition#oldExpressionInQuantifiers(JmlOldExpression)

getLocalVariablesInQuantifiedExpression

public void getLocalVariablesInQuantifiedExpression(java.lang.String evaluatorPUse)

Fetches local variables in quantified expression. It checks whether the variables are not in evaluatorPUse, and its binding is LocalVariable type.

setLocalVariables

public void setLocalVariables(java.lang.String str)

setLocalBindings

public void setLocalBindings(java.lang.String str)

getLocalVariables

public java.lang.String getLocalVariables()

getLocalBindings

public java.lang.String getLocalBindings()