|
JML | ||||||||||
| PREV NEXT | FRAMES NO FRAMES | ||||||||||
| Packages that use org.jmlspecs.jmlrac.qexpr | |
| org.jmlspecs.checker | Contains the source code for a parser and typechecker for JML annotations and java code. |
| org.jmlspecs.jmlrac | Generates Java classes from JML specifications that check assertions at runtime. |
| org.jmlspecs.jmlrac.qexpr | Translates JML quantified expressions into Java source code to evaluate them at runtime. |
| Classes in org.jmlspecs.jmlrac.qexpr used by org.jmlspecs.checker | |
| AbstractExpressionVisitor
An abstract visitor class that visits all subexpressions of a given expression recursively. |
|
| Classes in org.jmlspecs.jmlrac.qexpr used by org.jmlspecs.jmlrac | |
| AbstractExpressionVisitor
An abstract visitor class that visits all subexpressions of a given expression recursively. |
|
| Classes in org.jmlspecs.jmlrac.qexpr used by org.jmlspecs.jmlrac.qexpr | |
| AbstractExpressionVisitor
An abstract visitor class that visits all subexpressions of a given expression recursively. |
|
| NonExecutableQuantifierException
Thrown to indicate that an attempt has been made to translate a JML quantified expression that is not executable. |
|
| QInterval.Bound
A class for representing tuples of JExpression objects
and int values. |
|
| 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. |
|
| StaticAnalysis
An abstract class for translating JML quantified expressions into Java source code. |
|
| Translator
An abstract class for translating JML quantified expressions into Java source code. |
|
|
JML | ||||||||||
| PREV NEXT | FRAMES NO FRAMES | ||||||||||