Uses of Package
org.jmlspecs.jml4.rac

Packages that use org.jmlspecs.jml4.rac

org.jmlspecs.jml4.rac
org.jmlspecs.jml4.rac.quantifiedexpression

Classes in org.jmlspecs.jml4.rac used by org.jmlspecs.jml4.rac

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.

CodeBuffer
Improved version of the StringBuffer class.

ConstructorHeaderTranslator
Translates a constructor header along with its specification to a set of RAC methods.

DefaultRacAstVisitor
A concrete visitor class for the interface RacAstVisitor.

ExpressionTranslator
Translates various Java and JML expressions to RAC code.

InvariantLikeMethod
Generates assertion check methods for type assertions such as invariants and history constraints.

JavaAstVisitor
An AST Visitor interface for visiting every Java-type node.

JmlAstVisitor
An AST Visitor interface for visiting every Jml-type node.

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.

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.

PrePostconditionMethod
An abstract class for generating precondition or postconditin check methods for methods.

RacAstVisitor

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

RacConstants.Behavior
Different types of behavior for heavyweight specification

RacConstants.Condition
Different types of Rac condition

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.

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.

TypeAssertionTranslator
Translates type assertions such as invariants and history constraints.

TypeDeclarationTranslator
Translates JML assertions associated with types to runtime assertion checking (RAC) code.

VariableGenerator
A class for generating various unique variable names for RAC.

WrapperMethodGenerator
Generates a wrapper method.

Classes in org.jmlspecs.jml4.rac used by org.jmlspecs.jml4.rac.quantifiedexpression

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

PostStateExpressionTranslator
Translates various Java and JML expressions to RAC code that may contain JML old expressions.

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

RacResult
Data structure class to pass various RAC translation results to the caller.

VariableGenerator
A class for generating various unique variable names for RAC.