Package org.jmlspecs.jml4.rac

Interface Summary

JavaAstVisitor	An AST Visitor interface for visiting every Java-type node.
JmlAstVisitor	An AST Visitor interface for visiting every Jml-type node.
RacAstVisitor
RacConstants	A set of string constants used by RAC implementation classes.
TypeAssertionTranslator	Translates type assertions such as invariants and history constraints.

Class Summary

AssertionMethod	An abstract class to generate assertion check methods for various kinds of assertions such as preconditions, normal and exceptional postconditions, invariants, and history constraints.
AstDirtyBitsRestorer
AstDirtyBitsRetriever
AstMerger	Merges two compilation unit ASTs.
ClassDeclarationTranslator	Translates JML assertions associated with classes to runtime assertion checking (RAC) code.
CodeBuffer	Improved version of the StringBuffer class.
ConstraintMethod	Generates assertion check methods for history constraints.
ConstraintTranslator	Translates constraint clauses to history constraint checking methods.
ConstructorBodyTranslator	Translates JML in-line assertions or statements contained in a constructor to RAC code.
ConstructorHeaderTranslator	Translates a constructor header along with its specification to a set of RAC methods.
Debugger	Provides a bunch of utility methods for debugging RAC implementation.
DefaultRacAstVisitor	A concrete visitor class for the interface RacAstVisitor.
DesugarSpec	A JML visitor class for desugaring method specifications.
ExceptionalPostconditionMethod	Generate exceptional postcondition check methods.
ExceptionalPostconditionTranslator	Translate the exceptional postcondition of a method or constructor.
ExpressionTranslator	Translates various Java and JML expressions to RAC code.
InlineAssertionMerger	Merges RAC code of JML in-line assertions to their original assertions.
InlineAssertionTranslator	Translates in-line assertions o RAC code.
InlineAssertionVisitor	Visitor class to translate a JML in-line assertion into RAC code.
InterfaceDeclarationTranslator	Translates JML assertions associated with interfaces to runtime assertion checking (RAC) code.
InvariantLikeMethod	Generates assertion check methods for type assertions such as invariants and history constraints.
InvariantMethod	Generates assertion check methods for invariants.
InvariantTranslator	Translates invariants clauses to invariant checking methods.
JmlNullifier
Main	Command-line interface to the JML RAC compiler.
MethodBodyTranslator	Translates a method body of a class or interface to RAC code.
MethodDeclarationTranslator	Translate a method declaration into RAC code.
MethodHeaderTranslator	Translates a method or constructor header along with its specification such as pre and postconditions to a set of RAC methods.
MethodSpecificationTranslator	Translate a method declaration into RAC code.
PostconditionMethod	A class for generating postcondition check methods.
PostconditionTranslator
PostStateExpressionTranslator	Translates various Java and JML expressions to RAC code that may contain JML old expressions.
PreconditionMethod	Generates precondition check methods.
PreconditionTranslator	Translates the precondition of a method or constructor into RAC code.
PrePostconditionMethod	An abstract class for generating precondition or postconditin check methods for methods.
RacCompiler	A RAC compiler for JML.
RacConstructorDeclaration	A fake constructor declaration to store runtime assertion checking constructor in the source code format.
RacFieldDeclaration	A fake method declaration to store runtime assertion checking method in the source code format.
RacMethodDeclaration	A fake method declaration to store runtime assertion checking method in the source code format.
RacOldExpression	A RAC representation of a JML old expression.
RacOptions	Specifies RAC-specific compilation options.
RacParser
RacPrettyPrinter	Pretty prints RAC code.
RacResult	Data structure class to pass various RAC translation results to the caller.
RacTranslator	Abstract superclass defining several utility methods for RAC translation.
RacTypeDeclaration	A fake type declaration to store a runtime assertion class such as a surrogate class in the source code format.
ResolutionNullifier	A visitor to nullify various resolutions such as type binding done on JML AST nodes.
TypeDeclarationTranslator	Translates JML assertions associated with types to runtime assertion checking (RAC) code.
VariableGenerator	A class for generating various unique variable names for RAC.
WrapperConstructorGenerator	Generates a wrapper constructor.
WrapperMethodGenerator	Generates a wrapper method.

Enum Summary

RacConstants.Behavior	Different types of behavior for heavyweight specification
RacConstants.Condition	Different types of Rac condition

Exception Summary

NonExecutableException

Thrown to indicate that an attempt has been made to translate a JML expression that is not executable.