JML

Uses of Interface
org.jmlspecs.jmlrac.RacVisitor

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

JML is Copyright (C) 1998-2002 by Iowa State University and is distributed under the GNU General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version. This release depends on code from the MultiJava project and is based in part on the Kopi project Copyright (C) 1990-99 DMS Decision Management Systems Ges.m.b.H.