|
JML | ||||||||||
| PREV NEXT | FRAMES NO FRAMES | ||||||||||
| Packages that use JmlAbstractVisitor | |
| 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. |
| Uses of JmlAbstractVisitor in org.jmlspecs.checker |
| Subclasses of JmlAbstractVisitor in org.jmlspecs.checker | |
class |
JmlAdmissibilityVisitor
A visitor class to check admissibility of JML invariants and represents clauses. |
(package private) class |
JmlClassicalAdmissibilityVisitor
|
class |
JmlExpressionChecker
A visitor class to check privacy (and purity) of JML expressions. |
(package private) class |
JmlOwnershipAdmissibilityVisitor
|
| Uses of JmlAbstractVisitor in org.jmlspecs.jmlrac |
| Subclasses of JmlAbstractVisitor in org.jmlspecs.jmlrac | |
class |
AbstractExpressionTranslator
This class is intended to be a common base class for both TransExpression and TransExpression2. |
(package private) class |
AssertionMethod.AssertionMethod$1
|
class |
DesugarSpec
A JML visitor class for desugaring method specifications. |
class |
JmlRacGenerator
A class implementing the JML Runtime Assertion Checker (RAC). |
class |
RacAbstractVisitor
A default implementation for the RacVisitor interface. |
class |
TransConstructorBody
A visitor class for translating JML specification statements in a constrcutor body into assertion check code. |
class |
TransExpression
A RAC visitor class to translate JML expressions into Java source code. |
class |
TransExpression2
A RAC visitor class to translate JML expressions into Java source code. |
class |
TransExpressionSideEffect
A special expression translator that allows translation of expressions with side-effects. |
protected static class |
TransMethod.SpecCaseCollector
A class for collecting all specification cases from a desugared method specification. |
class |
TransMethodBody
A visitor class for translating JML specification statements in a method body into assertion check code. |
class |
TransOldExpression
A RAC visitor class for transforming JML old expressions into Java code. |
class |
TransPostcondition
A RAC visitor class for transforming JML postconditions into Java source code. |
private class |
TransPostcondition.QVarChecker
A class to check whether an expression has any references to quantified variables. |
class |
TransPostExpression2
A RAC visitor class to translate JML expressions into Java source code. |
private class |
TransPostExpression2.QVarChecker
A class to check whether an expression has any references to quantified variables. |
class |
TransPredicate
A RAC visitor class for transforming JML predicates into Java code. |
| Uses of JmlAbstractVisitor in org.jmlspecs.jmlrac.qexpr |
| Subclasses of JmlAbstractVisitor in org.jmlspecs.jmlrac.qexpr | |
class |
AbstractExpressionVisitor
An abstract visitor class that visits all subexpressions of a given expression recursively. |
private static class |
QInterval.CheckRecursion
A class to check an appearance of local variables in an expression. |
|
JML | ||||||||||
| PREV NEXT | FRAMES NO FRAMES | ||||||||||