Uses of Interface
org.jmlspecs.checker.Constants

Packages that use Constants

org.jmlspecs.checker	Contains the source code for a parser and typechecker for JML annotations and java code.
org.jmlspecs.jmldoc.jmldoc_142
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 Constants in org.jmlspecs.checker

Classes in org.jmlspecs.checker that implement Constants

class	CTypeType This class represents the JML \TYPE type.
class	JConstructorDeclarationWrapper A class representing a constructor declaration in the syntax tree.
class	JFieldDeclarationWrapper A class representing a field declaration in the syntax tree.
class	JInterfaceDeclarationWrapper This class represents a java interface in the syntax tree
class	JMethodDeclarationWrapper A class representing a method declaration in the syntax tree.
class	JmlAbruptSpecBody JmlAbruptSpecBody.java
class	JmlAbruptSpecCase JmlAbruptSpecCase.java
class	JmlAbstractVisitor An abstract JML visitor class to facilitate writing concrete visitor classes that implements the interface JmlVisitor.
class	JmlAccessibleClause An AST node class representing the JML accessible clause.
class	JmlAccumSubclassingInfo
class	JmlAdmissibilityVisitor A visitor class to check admissibility of JML invariants and represents clauses.
class	JmlAssertOrAssumeStatement This class represents the type of assert-statement, and assume-statement in JML.
class	JmlAssertStatement JmlAssertStatement.java
class	JmlAssignableClause A JML AST node for the assignable clause.
class	JmlAssignmentStatement JmlAssignmentStatement.java
class	JmlAssumeStatement JmlAssumeStatement.java
class	JmlAxiom This AST node represents a JML axiom annotation.
class	JmlBehaviorSpec JmlBehaviorSpec.java heavyweight-spec ::= [ privacy ] "behavior" generic-spec-case
class	JmlBinaryArithmeticExpressionHelper This class is an abstract root class for binary expressions.
class	JmlBinaryField This class represents a class read from a *.class file.
class	JmlBinaryMember This type represents a java declaration in the syntax tree.
class	JmlBinaryMethod This class represents a method read from a *.class file.
class	JmlBinarySourceClass This class represents a class read from a *.class file.
class	JmlBinaryType This class represents a class read from a *.class file.
class	JmlBreaksClause JmlBreaksClause.java
class	JmlCallableClause An AST node class representing the JML callable clause.
class	JmlCapturesClause An AST node class representing the JML captures clause.
class	JmlClassContext This class represents the context for a class during checking passes (checkInterface, checkInitializers, typecheck).
class	JmlClassDeclaration This type represents a java class declaration in the syntax tree.
(package private) class	JmlClassicalAdmissibilityVisitor
class	JmlClassOrGFImport This type represents (in the AST) import statements for single classes or generic functions, e.g., import java.util.ArrayList; or import org.multijava.samples.typecheck.
class	JmlCodeContract An abstraction of JML method specification.
class	JmlCompilationUnit This class represents a single JML compilation unit (typically a file in a file-based compiler like this) in the AST.
class	JmlCompilationUnitContext This class represents the context for a compilation unit during checking passes (checkInterface, checkInitializers, typecheck).
class	JmlConstraint This AST node represents a JML constraint annotation.
class	JmlConstructorContext This class represents the context for a constructor during checking passes (checkInterface, checkInitializers, typecheck).
class	JmlConstructorDeclaration JmlConstructorDeclaration.java
class	JmlConstructorName This AST node represents a constructor in a JML annotation.
class	JmlContext Descendents of this class represent local contexts during checking passes (checkInterface, checkInitializers, typecheck).
class	JmlContinuesClause JmlContinuesClause.java
class	JmlDataGroupClause This class represents a jml-var-assertion of the form initially predicate.
class	JmlDebugStatement A concrete AST node class to represent the debug statement of the following form: debug-statement ::= "debug" expression ;
class	JmlDeclaration This abstract class is the superclass of all jml-declaration AST nodes, (i.e., invariants, history constraints, depends declarations, and represents declarations)
class	JmlDivergesClause A JML AST node class for the diverges clause.
class	JmlDurationClause JmlDurationClause.java
class	JmlDurationExpression JmlDurationExpression.java
class	JmlElemTypeExpression JmlElemTypeExpression.java
class	JmlEnsuresClause A JML AST node for the <\code>ensures clause.
class	JmlExample A class representing JML example specifications.
class	JmlExceptionalBehaviorSpec JmlExceptionalBehaviorSpec.java heavyweight-spec ::= [ privacy ] "exceptional_behavior" exceptional-spec-case
class	JmlExceptionalExample A class representing JML exceptional example specifications.
class	JmlExceptionalSpecBody An AST node class for the JML exceptional-spec-body.
class	JmlExceptionalSpecCase An AST node class for the JML exceptional-spec-case.
class	JmlExpression JmlExpression.java
class	JmlExpressionChecker A visitor class to check privacy (and purity) of JML expressions.
class	JmlExpressionContext A class for representing the context in which JML expressions are typechecked.
class	JmlExtendingSpecification A method specification that extetends inherited specifications.
class	JmlFieldDeclaration JmlFieldDeclaration.java
class	JmlFlowControlContext This class is used during typechecking for control flow analysis that maintains local variable definite assignment (JLS2, 16), throwable, and reachability information (JLS2, 14.20).
class	JmlForAllVarDecl An AST node class for the JML forall variable declarations.
class	JmlFormalParameter This class represents a formal parameter in a JML AST.
class	JmlFreshExpression JmlFreshExpression.java
class	JmlGeneralSpecCase An abstraction of JML specification cases.
class	JmlGenericSpecBody An AST node class for the JML generic-spec-body.
class	JmlGenericSpecCase An AST node class for the JML generic-spec-case.
class	JmlHeavyweightSpec An AST node class for the JML heavyweight-spec.
class	JmlHenceByStatement JmlHenceByStatement.java
class	JmlInformalExpression JmlInformalExpression.java
class	JmlInformalStoreRef JmlInformalStoreRef.java
class	JmlInGroupClause This class represents a jml-var-assertion of the form initially predicate.
class	JmlInitializerContext This class represents the context for a static initializer during checking passes (checkInterface, checkInitializers, typecheck).
class	JmlInitiallyVarAssertion This class represents a jml-var-assertion of the form initially predicate.
class	JmlInterfaceContext This class represents the context for an interface declaration during checking passes (checkInterface, checkInitializers, typecheck).
class	JmlInterfaceDeclaration This class represents a java interface in the syntax tree
class	JmlInvariant This AST node represents a JML invariant annotation.
class	JmlInvariantForExpression AST for the JML expression \invariant_for.
class	JmlIsInitializedExpression AST for the JML expression \is_initialized.
class	JmlLabeled JmlLabeledClause.java
class	JmlLabelExpression AST for the JML expressions \lblneg and \lblpos.
class	JmlLetVarDecl An AST node class for the JML let (old) variable declarations.
class	JmlLockSetExpression AST for the JML expression \lockset.
class	JmlLoopInvariant JmlLoopInvariant.java
class	JmlLoopSpecification This is the super class for the classes representing loop-invariant and variant-function annotations for loop-stmt.
class	JmlLoopStatement This class represents loop-stmts annotated with loop-invariants and/or variant-functions.
class	JmlMapsIntoClause This class represents a jml-var-assertion of the form initially predicate.
class	JmlMaxExpression JmlMaxExpression.java
class	JmlMeasuredClause JmlMeasuredClause.java
class	JmlMemberAccess This class represents and contains the information needed to determine whether a member of a class or compilation unit can be accessed from some other member.
class	JmlMemberDeclaration This type represents a java declaration in the syntax tree.
class	JmlMethodContext This class represents the context for a method during checking passes (checkInterface, checkInitializers, typecheck).
class	JmlMethodDeclaration JmlMethodDeclaration.java
class	JmlMethodName This AST node represents a method name in a JML annotation.
class	JmlMethodNameList An AST node class representing the JML callable clause.
class	JmlMethodSpecification An abstraction of JML method specification.
class	JmlModelProgram JmlModelProgram.java
class	JmlMonitorsForVarAssertion JmlMonitorsForVarAssertion.java
class	JmlName This class represents a store-ref-name, store-ref-name-suffix, method-res-start, or identifier from a method-ref in an AST.
class	JmlNode This is the superclass of most JML AST nodes.
class	JmlNonNullElementsExpression JmlNonNullElementsExpression.java
class	JmlNormalBehaviorSpec JmlNormalBehaviorSpec.java heavyweight-spec ::= [ privacy ] "normal_behavior" normal-spec-case
class	JmlNormalExample A class representing JML normal example specifications.
class	JmlNormalSpecBody An AST node class for the JML normal-spec-body.
class	JmlNormalSpecCase An AST node class for the JML normal-spec-case.
class	JmlNotAssignedExpression JmlNotAssignedExpression.java
class	JmlNotModifiedExpression JmlNotModifiedExpression.java
class	JmlNumericType This class represents the JML primitive numeric types bigint and real.
class	JmlOldExpression JmlOldExpression.java
class	JmlOnlyAccessedExpression JmlOnlyAccessedExpression.java
class	JmlOnlyAssignedExpression JmlOnlyAssignedExpression.java
class	JmlOnlyCalledExpression JmlOnlyCalledExpression.java
class	JmlOnlyCapturedExpression JmlOnlyCapturedExpression.java
(package private) class	JmlOwnershipAdmissibilityVisitor
class	JmlPackageImport This type represents (in the AST) full-package import statements.
class	JmlPredicateClause JmlPredicateClause.java
class	JmlPreExpression JmlPreExpression.java
class	JmlQuotedExpressionWrapper This abstract class is the super class of all JmlExpressions that simply modify a quoted Java expression (e.g.
class	JmlReachExpression An AST node class for the JML reach expressions.
class	JmlReadableIfVarAssertion This class represents a jml-var-assertion of the form readable id if predicate.
class	JmlRedundantSpec A class representing JML redundant specifications.
class	JmlRefinePrefix
class	JmlRelationalExpression This class represents the JML relational expressions.
class	JmlRepresentsDecl This AST node represents a JML represents declaration annotation.
class	JmlRequiresClause JmlRequiresClause.java
class	JmlResultExpression JmlResultExpression.java
class	JmlReturnsClause JmlReturnsClause.java
class	JmlSetComprehension An AST node class for JML's set comprehension notation.
class	JmlSetStatement JmlSetStatement.java
class	JmlSigBinaryMethod A class to represent JML method declaratons read from bytecode files.
class	JmlSignalsClause A JML AST node class for the signals clause.
class	JmlSignalsOnlyClause A JML AST node class for the signals_only clause.
class	JmlSourceClass A class for representing JML classes read from *.java files.
class	JmlSourceField A class for representing an exported field of a class.
class	JmlSourceMethod A class for representing JML method declaration in the signature forest.
class	JmlSpaceExpression JmlSpaceExpression.java
class	JmlSpecBody JmlSpecBodyClause.java
class	JmlSpecBodyClause This abstract class is the common superclass of different kinds of specification clauses appearing in the specification body such as JmlAccessibleClause, JmlAssignableClause, JmlCallableClause, and JmlPredicateClause.
class	JmlSpecCase An abstraction of JML specification cases.
class	JmlSpecExpressionWrapper This abstract class is the super class of all JmlExpressions that simply modify a spec-expression (e.g.
class	JmlSpecification JmlSpecification.java
class	JmlSpecQuantifiedExpression An AST node class for JML quantified expressions.
class	JmlSpecStatementClause JmlSpecStatementClause.java
class	JmlSpecVarDecl An abstraction of JML specification variable declarations.
class	JmlStdType This class is a singleton that provides variables for the various built-in and java.lang types.
class	JmlStoreRef An abstraction of JML store references.
class	JmlStoreRefExpression An AST node class for JML store reference expressions.
class	JmlStoreRefKeyword This class represents a JmlStoreRefKeyword in the AST.
class	JmlStoreRefListWrapper JmlStoreRefListWrapper.java
class	JmlTypeDeclaration This type represents a java class or interface in the syntax tree.
class	JmlTypeExpression JmlTypeExpression.java
class	JmlTypeOfExpression JmlTypeOfExpression.java
class	JmlUnaryExpression This class represents unary expressions (unary plus, unary minus, bitwise complement, and logical not).
class	JmlVarAssertion This class represents jml-var-assertion in JML ASTs.
class	JmlVariableDefinition A wrapper of the class JVariableDefinition to store JML-specific information.
class	JmlVariantFunction JmlVariantFunction.java
class	JmlWhenClause JmlWhenClause.java
class	JmlWorkingSpaceClause JmlWorkingSpaceClause.java
class	JmlWorkingSpaceExpression JmlWorkingSpaceExpression.java
class	JmlWritableIfVarAssertion This class represents a jml-var-assertion of the form writable id if predicate.
class	JStatementWrapper An abstraction of JML statement ASTs that should be subclass of JStatement.
class	NonNullStatistics
class	TestJmlParser Unit tests for JmlParser

Uses of Constants in org.jmlspecs.jmldoc.jmldoc_142

Classes in org.jmlspecs.jmldoc.jmldoc_142 that implement Constants

class

SpecWriter This class is a Visitor class that generates appropriate portions of the javadoc documentation by walking the parse tree.

Uses of Constants in org.jmlspecs.jmlrac

Subinterfaces of Constants in org.jmlspecs.jmlrac

interface	RacConstants A set of string constants used by RAC implementation classes.
interface	RacVisitor An implementation of the Visitor Design Pattern [GoF94] for the JML runtime assertion checker.

Classes in org.jmlspecs.jmlrac that implement Constants

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.
(package private) class	AssertionMethod.AssertionMethod$1
class	ConstraintMethod A class for generating assertion check methods for (history) constraints.
class	ConstructorWrapper A class for generating constructor wrappers.
class	DesugarSpec A JML visitor class for desugaring method specifications.
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.
static class	RacParser.RacMethodDeclaration A RAC node class for representing method declarations.
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.
protected static class	TransMethod.SpecCaseCollector A class for collecting all specification cases from a desugared method specification.
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 Constants in org.jmlspecs.jmlrac.qexpr

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

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 Constants in org.jmlspecs.racwrap

Classes in org.jmlspecs.racwrap that implement Constants

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