Uses of Interface
org.jmlspecs.jmlrac.RacConstants

Packages that use RacConstants

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 RacConstants in org.jmlspecs.checker

Classes in org.jmlspecs.checker that implement RacConstants

class	JmlAdmissibilityVisitor A visitor class to check admissibility of JML invariants and represents clauses.
(package private) class	JmlClassicalAdmissibilityVisitor
(package private) class	JmlOwnershipAdmissibilityVisitor

Uses of RacConstants in org.jmlspecs.jmlrac

Subinterfaces of RacConstants 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 RacConstants

class	AbstractExpressionTranslator This class is intended to be a common base class for both TransExpression and TransExpression2.
class	AssertionMethod An abstract class for generating assertion check methods for specific kinds of assertions such as preconditions, normal and exceptional postconditions, invariants and (history) constraints.
class	ConstraintMethod A class for generating assertion check methods for (history) constraints.
class	ConstructorWrapper A class for generating constructor wrappers.
class	ExceptionalPostconditionMethod A class for generating exceptional postcondition check methods.
class	FinalizerWrapper A class for generating wrapper methods for finalizers.
class	InvariantLikeMethod A class for generating assertion check methods for class-level assertions such as invariants and history constraints.
class	InvariantMethod A class for generating assertion check methods for invariants.
class	JmlRacGenerator A class implementing the JML Runtime Assertion Checker (RAC).
class	LocalConstraintMethod A class for generating constaint check methods that check locally specified type constraints without inheriting any constraints from supertypes.
class	Main.JmlGenerateAssertionTask A task for generating runtime assertion checker (RAC) code.
class	MotherConstraintMethod A class for generating constraint check methods that check locally specified type constraints and inherit constraints from supertypes.
class	PostconditionMethod A class for generating postcondition check methods.
class	PreconditionMethod A class for generating precondition check methods.
class	PreOrPostconditionMethod An abstract class for generating precondition or postconditin check methods for the given methods.
(package private) class	PreValueVars A container class to store information about private fields that are used to pass pre-state values, typically computed by precondition check methods, to postcondition check methods.
class	RacAbstractVisitor A default implementation for the RacVisitor interface.
class	RacPrettyPrinter A visitor class for pretty-printing JML specifications with generated RAC code.
class	SubtypeConstraintMethod A class for generating constaint check methods that check locally specified type constraints and inherit constraints from supertypes.
class	TransClass A class for translating JML class declarations.
class	TransConstraint A class for translating JML (history) constraints.
class	TransConstructor A class for translating JML annotated constructor into a RAC-enabled method.
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	TransInterface A class for translating JML interface declarations.
class	TransInvariant A class for translating JML invariants.
class	TransMethod A class for translating JML annotated Java methods into RAC-enabled methods.
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.
class	TransType An abstract class for translating JML type declarations.
class	TransUtils A utility class for translating JML annotated Java classes into RAC-enabled classes.
class	VarGenerator A class for generating various uniques variable names for RAC.
private static class	VarGenerator.VarGenForClass A variable generator for classes.
private static class	VarGenerator.VarGenForMethod A variable generator for methods.
class	WrapperMethod A class for generating wrapper methods.

Uses of RacConstants in org.jmlspecs.jmlrac.qexpr

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

class	AbstractExpressionVisitor An abstract visitor class that visits all subexpressions of a given expression recursively.
(package private) class	QInterval A class for static approximations of the intervals for quantified variables of integeral types.
private static class	QInterval.CheckRecursion A class to check an appearance of local variables in an expression.
(package private) class	QSet An abstract class that represetns qsets of quantified expressions.
private static class	QSet.Composite An abstract qset class consisting of two other qset objects, e.g., union or intersection qsets.
private static class	QSet.Intersection A concrete qset class representating a qset that is an intersection of two qsets.
private static class	QSet.Leaf A concrete qset class consisting of only one JML expression.
private static class	QSet.Top A special, concrete qset class that represents the universe of all objects.
private static class	QSet.Union A concrete qset class representating a union of two qsets.
(package private) class	StaticAnalysis An abstract class for translating JML quantified expressions into Java source code.
private static class	StaticAnalysis.EnumerationBased A concrete class for translating JML quantified expressions into Java source code.
private static class	StaticAnalysis.IntervalBased A concrete class for translating JML quantified expressions into Java source code.
private static class	StaticAnalysis.SetBased A concrete class for translating JML quantified expressions into Java source code.
(package private) class	Translator An abstract class for translating JML quantified expressions into Java source code.

Uses of RacConstants in org.jmlspecs.racwrap

Classes in org.jmlspecs.racwrap that implement RacConstants

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