|
JML | ||||||||||
| PREV NEXT | FRAMES NO FRAMES | ||||||||||
| Packages that use RacVisitor | |
| 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. |
| org.jmlspecs.racwrap | |
| Uses of RacVisitor in org.jmlspecs.checker |
| Classes in org.jmlspecs.checker that implement RacVisitor | |
class |
JmlAdmissibilityVisitor
A visitor class to check admissibility of JML invariants and represents clauses. |
(package private) class |
JmlClassicalAdmissibilityVisitor
|
(package private) class |
JmlOwnershipAdmissibilityVisitor
|
| Uses of RacVisitor in org.jmlspecs.jmlrac |
| Classes in org.jmlspecs.jmlrac that implement RacVisitor | |
class |
AbstractExpressionTranslator
This class is intended to be a common base class for both TransExpression and TransExpression2. |
class |
JmlRacGenerator
A class implementing the JML Runtime Assertion Checker (RAC). |
class |
RacAbstractVisitor
A default implementation for the RacVisitor interface. |
class |
RacPrettyPrinter
A visitor class for pretty-printing JML specifications with generated RAC code. |
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. |
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 RacVisitor in org.jmlspecs.jmlrac.qexpr |
| Classes in org.jmlspecs.jmlrac.qexpr that implement RacVisitor | |
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. |
| Uses of RacVisitor in org.jmlspecs.racwrap |
| Classes in org.jmlspecs.racwrap that implement RacVisitor | |
(package private) class |
OrigPrettyPrinter
|
class |
WrapperPrettyPrinter
WrapperPrettyPrinter prints the wrapper. |
|
JML | ||||||||||
| PREV NEXT | FRAMES NO FRAMES | ||||||||||