JML

Package org.jmlspecs.jmlrac.qexpr

Translates JML quantified expressions into Java source code to evaluate them at runtime.

See:
          Description

Class Summary
AbstractExpressionVisitor An abstract visitor class that visits all subexpressions of a given expression recursively.
QInterval A class for static approximations of the intervals for quantified variables of integeral types.
QInterval.Bound A class for representing tuples of JExpression objects and int values.
QInterval.CheckRecursion A class to check an appearance of local variables in an expression.
QSet An abstract class that represetns qsets of quantified expressions.
QSet.Composite An abstract qset class consisting of two other qset objects, e.g., union or intersection qsets.
QSet.Intersection A concrete qset class representating a qset that is an intersection of two qsets.
QSet.Leaf A concrete qset class consisting of only one JML expression.
QSet.Top A special, concrete qset class that represents the universe of all objects.
QSet.Union A concrete qset class representating a union of two qsets.
StaticAnalysis An abstract class for translating JML quantified expressions into Java source code.
StaticAnalysis.EnumerationBased A concrete class for translating JML quantified expressions into Java source code.
StaticAnalysis.IntervalBased A concrete class for translating JML quantified expressions into Java source code.
StaticAnalysis.SetBased A concrete class for translating JML quantified expressions into Java source code.
Translator An abstract class for translating JML quantified expressions into Java source code.
TransQuantifiedExpression An abstract class for translating JML quantified expressions into Java source code.
 

Exception Summary
NonExecutableQuantifierException Thrown to indicate that an attempt has been made to translate a JML quantified expression that is not executable.
 

Package org.jmlspecs.jmlrac.qexpr Description

Translates JML quantified expressions into Java source code to evaluate them at runtime. All three forms of JML quantified expressions are supported in translation.

This package provides a framework for translating quantified expressions using various translation approaches such as static analysis and type extension. Currently, however, the package supports only the static analysis approach. To use translate a quantified expression, one has to create an object of class TransQuantifiedExpression by passing appropriate arguments and invoke the method translate.

The classes in the package are organized as follows.

Translator {abstract} <---- TransQuantifiedExpression
  StaticAnalysis {abstract}
     EnumerationBased
     IntervalBased ----> QInterval --1,2--> 1. Bound
     SetBased ----> QSet <------+
                      Top       |
                      Leaf      |
                      Composite-+
                        Union
                        Intersection
AbstractExpressionVisitor {abstract}
   2. CheckRecursion

Related Documentation

For syntax, semantics, and examples of JML quantified expressions, please refer to:


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.