Uses of Package
org.jmlspecs.jmlrac

Packages that use org.jmlspecs.jmlrac

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

Classes in org.jmlspecs.jmlrac used by org.jmlspecs.checker

RacAbstractVisitor
A default implementation for the RacVisitor interface.

RacConstants
A set of string constants used by RAC implementation classes.

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

Classes in org.jmlspecs.jmlrac used by org.jmlspecs.jmlrac

AbstractExpressionTranslator
This class is intended to be a common base class for both TransExpression and TransExpression2.

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.

ConstraintMethod
A class for generating assertion check methods for (history) constraints.

InvariantLikeMethod
A class for generating assertion check methods for class-level assertions such as invariants and history constraints.

JmlModifier
A class providing utilities for operating on modifier bit masks.

JmlRacGenerator
A class implementing the JML Runtime Assertion Checker (RAC).

Main
A class implementing the entry point of the JML RAC compiler.

Main.JmlPrettyPrintTask
A task class for pretty-printing the trees in the AST forest.

MotherConstraintMethod
A class for generating constraint check methods that check locally specified type constraints and inherit constraints from supertypes.

PositionnedExpressionException
This is exception is used to report expressions evaluation issues encountered during the visit of the tree.

PostconditionMethod
A class for generating postcondition check methods.

PreOrPostconditionMethod
An abstract class for generating precondition or postconditin check methods for the given methods.

PreOrPostconditionMethod.StringPair
A record class that can store a pair of strings.

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.

PreValueVars.Entry
A data structure class to hold information about a field.

RacAbstractVisitor
A default implementation for the RacVisitor interface.

RacConstants
A set of string constants used by RAC implementation classes.

RacContext
A class for representing contexts for translating JML expressions.

RacGUI
This class is automatically generated from RacGUI.gui and contains member fields corresponding to tool-specific GUI specifications.

RacNode
An abstraction of RAC AST nodes.

RacOptions
This class is automatically generated from RacOptions.opt and contains member fields corresponding to command-line options.

RacParser.RacBlock
A RAC node class for representing blocks.

RacParser.RacMethodDeclaration
A RAC node class for representing method declarations.

RacParser.RacStatement
A RAC node class for representing statements.

RacPredicate
An AST node class for RAC-specific predicates.

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

TransExpression
A RAC visitor class to translate JML expressions into Java source code.

TransExpression.DynamicCallArg
A private data structure class for stroring information about arguments for dynamic calls.

TransExpression.StringAndNodePair
A private data structure class for stroring a pair of String and RacNode objects.

TransExpression2
A RAC visitor class to translate JML expressions into Java source code.

TransInvariant
A class for translating JML invariants.

TransMethod
A class for translating JML annotated Java methods into RAC-enabled methods.

TransMethod.SpecCase
An abstract superclass for conjoining multiple specification clauses, such as requires and ensures clauses, in a specification case.

TransMethodBody
A visitor class for translating JML specification statements in a method body into assertion check code.

TransPostcondition
A RAC visitor class for transforming JML postconditions into Java source code.

TransPostExpression2
A RAC visitor class to translate JML expressions into Java source code.

TransPredicate
A RAC visitor class for transforming JML predicates into Java code.

TransType
An abstract class for translating JML type declarations.

TransUtils
A utility class for translating JML annotated Java classes into RAC-enabled classes.

VarGenerator
A class for generating various uniques variable names for RAC.

WrapperMethod
A class for generating wrapper methods.

Classes in org.jmlspecs.jmlrac used by org.jmlspecs.jmlrac.qexpr

AbstractExpressionTranslator
This class is intended to be a common base class for both TransExpression and TransExpression2.

RacAbstractVisitor
A default implementation for the RacVisitor interface.

RacConstants
A set of string constants used by RAC implementation classes.

RacContext
A class for representing contexts for translating JML expressions.

RacNode
An abstraction of RAC AST nodes.

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

VarGenerator
A class for generating various uniques variable names for RAC.

Classes in org.jmlspecs.jmlrac used by org.jmlspecs.racwrap

JmlModifier
A class providing utilities for operating on modifier bit masks.

Main
A class implementing the entry point of the JML RAC compiler.

RacConstants
A set of string constants used by RAC implementation classes.

RacPrettyPrinter
A visitor class for pretty-printing JML specifications with generated RAC code.

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