JML

org.jmlspecs.jmlrac.qexpr
Class TransQuantifiedExpression

java.lang.Object
  extended byorg.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]]
        }
     }
 
The translation rules for other quantifiers are defined in a similar way.

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

Constructor Detail

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.
Method Detail

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.


JML

JML is Copyright (C) 1998-2002 by Iowa State University and is distributed under the GNU General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version. This release depends on code from the MultiJava project and is based in part on the Kopi project Copyright (C) 1990-99 DMS Decision Management Systems Ges.m.b.H.