org.jmlspecs.jmlrac.qexpr
Class TransQuantifiedExpression

java.lang.Object
  org.jmlspecs.jmlrac.qexpr.TransQuantifiedExpression

public class TransQuantifiedExpression

extends 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]]
        }
     }
 

Version:

$Revision: 1.16 $

Author:

Yoonsik Cheon

See Also:

TransExpression.visitJmlSpecQuantifiedExpression( JmlSpecQuantifiedExpression)

Field Summary
private  RacContext	context           Current translation context.
private  JmlSpecQuantifiedExpression	quantiExp           quantified expression to be translated.
private  String	resultVar           variable name to store the value of quantified expression in the translated code.
private  AbstractExpressionTranslator	transExp           translator for translating subexpressions
private  VarGenerator	varGen           variable generator for generating unique local variables.

 

Constructor Summary

TransQuantifiedExpression(VarGenerator varGen, RacContext context, JmlSpecQuantifiedExpression expr, String resultVar, AbstractExpressionTranslator transExp)           Constructs a new instance.

 

Method Summary
RacNode	generateLoop(RacNode 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.
private  RacNode	nonExecutableQuantifiedExpression()           Translates a non-executable quantified expression.
RacNode	translate()           Translates a JML quantified expression into Java source code and return the translated code.

 

Methods inherited from class java.lang.Object

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

 

Field Detail

varGen

private VarGenerator varGen

variable generator for generating unique local variables.

context

private RacContext context

Current translation context.

quantiExp

private JmlSpecQuantifiedExpression quantiExp

quantified expression to be translated.

resultVar

private String resultVar

variable name to store the value of quantified expression in the translated code.

transExp

private AbstractExpressionTranslator transExp

translator for translating subexpressions

TransQuantifiedExpression

public TransQuantifiedExpression(VarGenerator varGen,
                                 RacContext context,
                                 JmlSpecQuantifiedExpression expr,
                                 String resultVar,
                                 AbstractExpressionTranslator transExp)

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.

translate

public RacNode translate()

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

Returns:

translated Java source code.

Throws:

if - the quantified expression is not executable.

generateLoop

public RacNode generateLoop(RacNode 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)

nonExecutableQuantifiedExpression

private RacNode nonExecutableQuantifiedExpression()

Translates a non-executable quantified expression. A boolean-typed quantified expression is translated into resultVar = true/false;, if the contextual translation is enabled. Otherwise, it is translated into the following code:

  if (true) {
    throw new JMLNonExecutableException();
  }
 

A non-boolean typed quantified expression is also translated into the above if statement.