
JML  
PREV PACKAGE NEXT PACKAGE  FRAMES NO FRAMES 
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. 
Translates JML quantified expressions into Java source code to evaluate them at runtime. All three forms of JML quantified expressions are supported in translation.
\forall
and
\exists
)
\sum
, \product
,
\min
, and \max
)
\num_of
)
boolean
type.
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
.
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.
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

JML  
PREV PACKAGE NEXT PACKAGE  FRAMES NO FRAMES 