JML

Package org.jmlspecs.jmlrac

Generates Java classes from JML specifications that check assertions at runtime.

See:
          Description

Interface Summary
RacConstants A set of string constants used by RAC implementation classes.
RacNode An abstraction of RAC AST nodes.
RacVisitor An implementation of the Visitor Design Pattern [GoF94] for the JML runtime assertion checker.
 

Class Summary
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.
ConstructorWrapper A class for generating constructor wrappers.
DesugarSpec A JML visitor class for desugaring method specifications.
ExceptionalPostconditionMethod A class for generating exceptional postcondition check methods.
FinalizerWrapper A class for generating wrapper methods for finalizers.
InvariantLikeMethod A class for generating assertion check methods for class-level assertions such as invariants and history constraints.
InvariantMethod A class for generating assertion check methods for invariants.
JmlModifier A class providing utilities for operating on modifier bit masks.
JmlRacGenerator A class implementing the JML Runtime Assertion Checker (RAC).
JMLRacWarningFilter A warning filter for JML.
LocalConstraintMethod A class for generating constaint check methods that check locally specified type constraints without inheriting any constraints from supertypes.
Main A class implementing the entry point of the JML RAC compiler.
MotherConstraintMethod A class for generating constraint check methods that check locally specified type constraints and inherit constraints from supertypes.
PostconditionMethod A class for generating postcondition check methods.
PreconditionMethod A class for generating precondition 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.
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.
RacMessages  
RacOptions This class is automatically generated from RacOptions.opt and contains member fields corresponding to command-line options.
RacParser A utility class for generating RAC nodes from a string and an array of RAC/JML nodes.
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.
RacPrettyPrinter A visitor class for pretty-printing JML specifications with generated RAC code.
SubtypeConstraintMethod A class for generating constaint check methods that check locally specified type constraints and inherit constraints from supertypes.
TransClass A class for translating JML class declarations.
TransConstraint A class for translating JML (history) constraints.
TransConstructor A class for translating JML annotated constructor into a RAC-enabled method.
TransConstructorBody A visitor class for translating JML specification statements in a constrcutor body into assertion check code.
TransExpression A RAC visitor class to translate JML expressions into Java source code.
TransExpression.DiagTerm A class representing a term to be presented when an assertion is violated.
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.
TransExpressionSideEffect A special expression translator that allows translation of expressions with side-effects.
TransInterface A class for translating JML interface declarations.
TransInvariant A class for translating JML invariants.
TransMethod A class for translating JML annotated Java methods into RAC-enabled methods.
TransMethod.GeneralSpecCase A concrete wrapper class to JmlGeneralSpecCase for conjoining multiple specification clauses in a specification case.
TransMethod.SpecCase An abstract superclass for conjoining multiple specification clauses, such as requires and ensures clauses, in a specification case.
TransMethod.SpecCaseCollector A class for collecting all specification cases from a desugared method specification.
TransMethodBody A visitor class for translating JML specification statements in a method body into assertion check code.
TransOldExpression A RAC visitor class for transforming JML old expressions into Java 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.
VarGenerator.VarGenForClass A variable generator for classes.
VarGenerator.VarGenForMethod A variable generator for methods.
WrapperMethod A class for generating wrapper methods.
 

Exception Summary
NonExecutableExpressionException This is exception is used to report non-executable expressions when encountered during the visit of the tree.
NotImplementedExpressionException This is exception is used to report not implemented expressions when encountered during the visit of the tree.
NotSupportedExpressionException This is exception is used to report not supported expressions when encountered during the visit of the tree.
PositionnedExpressionException This is exception is used to report expressions evaluation issues encountered during the visit of the tree.
 

Package org.jmlspecs.jmlrac Description

Generates Java classes from JML specifications that check assertions at runtime. The runtime assertion checker allows one to check the Java Modeling Language (JML) assertions at runtime when the programs are being executed. It adds assertion check code to the generated Java bytecode that checks pre- and postconditions, invariants, and history constraints.

Related Documentation

The following short paper gives a quick overview on the JML's runtime assertion checker. For an overview, syntax, informal semantics, and examples of the JML language, please refer to:


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.