Uses of Interface
org.jmlspecs.checker.JmlVisitor

Packages that use JmlVisitor

org.jmlspecs.checker	Contains the source code for a parser and typechecker for JML annotations and java code.
org.jmlspecs.jmldoc.jmldoc_142
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 JmlVisitor in org.jmlspecs.checker

Classes in org.jmlspecs.checker that implement JmlVisitor

class	JmlAbstractVisitor An abstract JML visitor class to facilitate writing concrete visitor classes that implements the interface JmlVisitor.
class	JmlAccumSubclassingInfo
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
class	JmlVisitorNI Implementation of Visitor Design Pattern for KJC.

Uses of JmlVisitor in org.jmlspecs.jmldoc.jmldoc_142

Classes in org.jmlspecs.jmldoc.jmldoc_142 that implement JmlVisitor

class

SpecWriter This class is a Visitor class that generates appropriate portions of the javadoc documentation by walking the parse tree.

Uses of JmlVisitor in org.jmlspecs.jmlrac

Subinterfaces of JmlVisitor in org.jmlspecs.jmlrac

interface

RacVisitor An implementation of the Visitor Design Pattern [GoF94] for the JML runtime assertion checker.

Classes in org.jmlspecs.jmlrac that implement JmlVisitor

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	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.
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 JmlVisitor in org.jmlspecs.jmlrac.qexpr

Classes in org.jmlspecs.jmlrac.qexpr that implement JmlVisitor

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 JmlVisitor in org.jmlspecs.racwrap

Classes in org.jmlspecs.racwrap that implement JmlVisitor

(package private) class	OrigPrettyPrinter
class	WrapperPrettyPrinter WrapperPrettyPrinter prints the wrapper.