org.jmlspecs.jmlrac.qexpr (JML and MultiJava documentation)

Overview

Package

Class

Use

Tree

Deprecated

Index

Help

JML

PREV PACKAGE NEXT PACKAGE

FRAMES NO FRAMES

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.

Universal and existential quantifiers (\forall and \exists)
Generalized quantifiers (\sum, \product, \min, and \max)
Numerical quantifier (\num_of)

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.

Explicit Enumeration. All possible values of a quantified variable's type are explicitly enumerated. This works for at least the boolean type.
Interval Based. A range of possible values is statically determined by analyzing the predicate part of the quantified expression. For example, if the predicate part of a quantified expression is 0 <= x && x <= 10 with a quantified variable x, it is sufficient to test the expression part only for values between 0 and 10 inclusive to decide the value of the quantified expression. This approach works for such types as byte, char, short, int, and long.
Set Based. A set of possible objects is statically determined by analyzing the predicate part of the quantified expression. For example, if the predicate part of a quantified expression is c1.contains(x) || c2.contains(y), where x is a quantified variable and c1 and c2 are objects of some collection types, it is sufficient to test the expression part only for elements from the collections c1 and c2 to decide the value of the quantified expression. This approach works for all reference types.

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

Package org.jmlspecs.jmlrac.qexpr

Package org.jmlspecs.jmlrac.qexpr Description

Related Documentation