Uses of Package
org.jmlspecs.checker

Packages that use org.jmlspecs.checker

org.jmlspecs.checker	Contains the source code for a parser and typechecker for JML annotations and java code.
org.jmlspecs.jmldoc	The jmldoc tool documents java programs that contain JML (Java Modeling Language) annotations included as specially formatted comments; the generated html pages are very similar to those produced by javadoc, but with annotation information added.
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.jmlspec	A tool that can generate or compare specification skeletons from Java source or class files.
org.jmlspecs.jmlunit	Generates JUnit test classes from JML specifications.
org.jmlspecs.racwrap

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

Constants
Defines all additional constants shared by JML package files.

CParseClassContext
This class is used by the parser to collect the members of a class declaration.

CTypeType
This class represents the JML \TYPE type.

JavadocJmlLexerTokenTypes

JavadocJmlTokenTypes

JClassDeclarationWrapper
A wrapper class to JClassDeclaration to implement JML-specific typechecking.

JInterfaceDeclarationWrapper
This class represents a java interface in the syntax tree

JmlAbruptSpecBody
JmlAbruptSpecBody.java

JmlAbruptSpecCase
JmlAbruptSpecCase.java

JmlAbstractVisitor
An abstract JML visitor class to facilitate writing concrete visitor classes that implements the interface JmlVisitor.

JmlAccessibleClause
An AST node class representing the JML accessible clause.

JmlAdmissibilityVisitor
A visitor class to check admissibility of JML invariants and represents clauses.

JmlAdmissibilityVisitor.NotAdmissibleException
An Exception which is thrown when some was found not to be admissible.

JmlAssertOrAssumeStatement
This class represents the type of assert-statement, and assume-statement in JML.

JmlAssertStatement
JmlAssertStatement.java

JmlAssignableClause
A JML AST node for the assignable clause.

JmlAssignableFieldSet
This class acts as a set containing the assignable fields mentioned in an assignable clause.

JmlAssignmentStatement
JmlAssignmentStatement.java

JmlAssumeStatement
JmlAssumeStatement.java

JmlAxiom
This AST node represents a JML axiom annotation.

JmlBehaviorSpec
JmlBehaviorSpec.java heavyweight-spec ::= [ privacy ] "behavior" generic-spec-case

JmlBinaryMember
This type represents a java declaration in the syntax tree.

JmlBinarySourceClass
This class represents a class read from a *.class file.

JmlBinaryType
This class represents a class read from a *.class file.

JmlBreaksClause
JmlBreaksClause.java

JmlCallableClause
An AST node class representing the JML callable clause.

JmlCapturesClause
An AST node class representing the JML captures clause.

JmlClassBlock
This class represents a instance or static initializer block annotated with a JML method specification.

JmlClassContext
This class represents the context for a class during checking passes (checkInterface, checkInitializers, typecheck).

JmlClassDeclaration
This type represents a java class declaration in the syntax tree.

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.

JmlCodeContract
An abstraction of JML method specification.

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

JmlCompilationUnit
This class represents a single JML compilation unit (typically a file in a file-based compiler like this) in the AST.

JmlConstraint
This AST node represents a JML constraint annotation.

JmlConstructorDeclaration
JmlConstructorDeclaration.java

JmlConstructorName
This AST node represents a constructor in a JML annotation.

JmlContext
Descendents of this class represent local contexts during checking passes (checkInterface, checkInitializers, typecheck).

JmlContinuesClause
JmlContinuesClause.java

JmlDataGroupAccumulator
This class represents a set of jml-data-group-assertion's in JML ASTs.

JmlDataGroupClause
This class represents a jml-var-assertion of the form initially predicate.

JmlDataGroupMemberMap
This class acts as a

JmlDebugStatement
A concrete AST node class to represent the debug statement of the following form: debug-statement ::= "debug" expression ;

JmlDeclaration
This abstract class is the superclass of all jml-declaration AST nodes, (i.e., invariants, history constraints, depends declarations, and represents declarations)

JmlDivergesClause
A JML AST node class for the diverges clause.

JmlDurationClause
JmlDurationClause.java

JmlDurationExpression
JmlDurationExpression.java

JmlElemTypeExpression
JmlElemTypeExpression.java

JmlEnsuresClause
A JML AST node for the <\code>ensures clause.

JmlEqualityExpression
This class represents the AST node for the equality operators.

JmlExample
A class representing JML example specifications.

JmlExceptionalBehaviorSpec
JmlExceptionalBehaviorSpec.java heavyweight-spec ::= [ privacy ] "exceptional_behavior" exceptional-spec-case

JmlExceptionalExample
A class representing JML exceptional example specifications.

JmlExceptionalSpecBody
An AST node class for the JML exceptional-spec-body.

JmlExceptionalSpecCase
An AST node class for the JML exceptional-spec-case.

JmlExpression
JmlExpression.java

JmlExpressionContext
A class for representing the context in which JML expressions are typechecked.

JmlExprIDTokenTypes

JmlExtendingSpecification
A method specification that extetends inherited specifications.

JmlFieldDeclaration
JmlFieldDeclaration.java

JmlFileFinder
This FileFinder looks for a .class file and a .java file, returning whichever one is newer.

JmlForAllVarDecl
An AST node class for the JML forall variable declarations.

JmlFormalParameter
This class represents a formal parameter in a JML AST.

JmlFreshExpression
JmlFreshExpression.java

JmlGeneralSpecCase
An abstraction of JML specification cases.

JmlGenericSpecBody
An AST node class for the JML generic-spec-body.

JmlGenericSpecCase
An AST node class for the JML generic-spec-case.

JmlGuardedStatement
JmlGuardedStatement.java

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

JmlHeavyweightSpec
An AST node class for the JML heavyweight-spec.

JmlHenceByStatement
JmlHenceByStatement.java

JmlIDTokenTypes

JmlInformalExpression
JmlInformalExpression.java

JmlInformalStoreRef
JmlInformalStoreRef.java

JmlInGroupClause
This class represents a jml-var-assertion of the form initially predicate.

JmlInitiallyVarAssertion
This class represents a jml-var-assertion of the form initially predicate.

JmlInterfaceDeclaration
This class represents a java interface in the syntax tree

JmlInvariant
This AST node represents a JML invariant annotation.

JmlInvariantForExpression
AST for the JML expression \invariant_for.

JmlInvariantStatement
JmlInvariantStatement.java

JmlIsInitializedExpression
AST for the JML expression \is_initialized.

JmlJDLexerTokenTypes

JmlLabeled
JmlLabeledClause.java

JmlLabelExpression
AST for the JML expressions \lblneg and \lblpos.

JmlLetVarDecl
An AST node class for the JML let (old) variable declarations.

JmlLexer
This is the top level JML scanner.

JmlLexerTokenTypes

JmlLockSetExpression
AST for the JML expression \lockset.

JmlLoopInvariant
JmlLoopInvariant.java

JmlLoopSpecification
This is the super class for the classes representing loop-invariant and variant-function annotations for loop-stmt.

JmlLoopStatement
This class represents loop-stmts annotated with loop-invariants and/or variant-functions.

JmlMapsIntoClause
This class represents a jml-var-assertion of the form initially predicate.

JMLMathMode

JmlMaxExpression
JmlMaxExpression.java

JmlMeasuredClause
JmlMeasuredClause.java

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.

JmlMemberDeclaration
This type represents a java declaration in the syntax tree.

JmlMethodContext
This class represents the context for a method during checking passes (checkInterface, checkInitializers, typecheck).

JmlMethodDeclaration
JmlMethodDeclaration.java

JmlMethodName
This AST node represents a method name in a JML annotation.

JmlMethodNameList
An AST node class representing the JML callable clause.

JmlMethodSpecification
An abstraction of JML method specification.

JmlMLLexer
This is the scanner for multi-line JML annotations.

JmlMLLexerTokenTypes

JmlModelProgram
JmlModelProgram.java

JmlModelProgStatement
The type of model-prog-statements.

JmlMonitorsForVarAssertion
JmlMonitorsForVarAssertion.java

JmlName
This class represents a store-ref-name, store-ref-name-suffix, method-res-start, or identifier from a method-ref in an AST.

JmlNode
This is the superclass of most JML AST nodes.

JmlNondetChoiceStatement
JmlNondetChoiceStatement.java

JmlNondetIfStatement
JmlNondetIfStatement.java

JmlNonNullElementsExpression
JmlNonNullElementsExpression.java

JmlNormalBehaviorSpec
JmlNormalBehaviorSpec.java heavyweight-spec ::= [ privacy ] "normal_behavior" normal-spec-case

JmlNormalExample
A class representing JML normal example specifications.

JmlNormalSpecBody
An AST node class for the JML normal-spec-body.

JmlNormalSpecCase
An AST node class for the JML normal-spec-case.

JmlNotAssignedExpression
JmlNotAssignedExpression.java

JmlNotModifiedExpression
JmlNotModifiedExpression.java

JmlNumericType
This class represents the JML primitive numeric types bigint and real.

JmlOldExpression
JmlOldExpression.java

JmlOnlyAccessedExpression
JmlOnlyAccessedExpression.java

JmlOnlyAssignedExpression
JmlOnlyAssignedExpression.java

JmlOnlyCalledExpression
JmlOnlyCalledExpression.java

JmlOnlyCapturedExpression
JmlOnlyCapturedExpression.java

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

JmlOwnershipAdmissibilityVisitor

JmlPackageImport
This type represents (in the AST) full-package import statements.

JmlParser

JmlParser.TypeBooleanPair

JmlParser.TypeWeaklyList
This nested class represents a list of implemented interfaces for a class declaration (or extends interfaces for an interface declaration) and whether they are implemented (or extended) weakly.

JmlPredicate
This represents the AST node for a predicate in JML.

JmlPredicateClause
JmlPredicateClause.java

JmlPredicateKeyword

JmlPreExpression
JmlPreExpression.java

JmlQuotedExpressionWrapper
This abstract class is the super class of all JmlExpressions that simply modify a quoted Java expression (e.g.

JmlReachExpression
An AST node class for the JML reach expressions.

JmlReadableIfVarAssertion
This class represents a jml-var-assertion of the form readable id if predicate.

JmlRedundantSpec
A class representing JML redundant specifications.

JmlRefinePrefix

JmlRelationalExpression
This class represents the JML relational expressions.

JmlRepresentsDecl
This AST node represents a JML represents declaration annotation.

JmlRequiresClause
JmlRequiresClause.java

JmlResultExpression
JmlResultExpression.java

JmlReturnsClause
JmlReturnsClause.java

JmlSetComprehension
An AST node class for JML's set comprehension notation.

JmlSetStatement
JmlSetStatement.java

JmlSigClassCreator
A concrete class creator to create JML classes from bytecode files.

JmlSignalsClause
A JML AST node class for the signals clause.

JmlSignalsOnlyClause
A JML AST node class for the signals_only clause.

JmlSLLexer

JmlSLLexerTokenTypes

JmlSourceClass
A class for representing JML classes read from *.java files.

JmlSourceField
A class for representing an exported field of a class.

JmlSourceMethod
A class for representing JML method declaration in the signature forest.

JmlSpaceExpression
JmlSpaceExpression.java

JmlSpecBody
JmlSpecBodyClause.java

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.

JmlSpecCase
An abstraction of JML specification cases.

JmlSpecExpression

JmlSpecExpressionWrapper
This abstract class is the super class of all JmlExpressions that simply modify a spec-expression (e.g.

JmlSpecification
JmlSpecification.java

JmlSpecQuantifiedExpression
An AST node class for JML quantified expressions.

JmlSpecStatement
JmlSpecStatement.java

JmlSpecStatementClause
JmlSpecStatementClause.java

JmlSpecVarDecl
An abstraction of JML specification variable declarations.

JmlStoreRef
An abstraction of JML store references.

JmlStoreRefExpression
An AST node class for JML store reference expressions.

JmlStoreRefKeyword
This class represents a JmlStoreRefKeyword in the AST.

JmlStoreRefListWrapper
JmlStoreRefListWrapper.java

JmlTokenTypes

JmlTopIDTokenTypes

JmlTypeDeclaration
This type represents a java class or interface in the syntax tree.

JmlTypeExpression
JmlTypeExpression.java

JmlTypeLoader
This class acts as a symbol table and a cache for types, type signatures, and external generic functions.

JmlTypeOfExpression
JmlTypeOfExpression.java

JmlUnreachableStatement
JmlUnreachableStatement.java

JmlVarAssertion
This class represents jml-var-assertion in JML ASTs.

JmlVariableDefinition
A wrapper of the class JVariableDefinition to store JML-specific information.

JmlVariantFunction
JmlVariantFunction.java

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

JmlVisitor
Implementation of Visitor Design Pattern for KJC.

JmlVisitorNI
Implementation of Visitor Design Pattern for KJC.

JMLWarningFilter
A warning filter for JML.

JmlWhenClause
JmlWhenClause.java

JmlWorkingSpaceClause
JmlWorkingSpaceClause.java

JmlWorkingSpaceExpression
JmlWorkingSpaceExpression.java

JmlWritableIfVarAssertion
This class represents a jml-var-assertion of the form writable id if predicate.

JStatementWrapper
An abstraction of JML statement ASTs that should be subclass of JStatement.

Main
This class implements the entry point of the JML compiler.

Main.PTMode

TestJmlParser.Helper

TokenStreamSelector
Provides for switching between various lexical analyzers for lexing JML.

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

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

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

Classes in org.jmlspecs.checker used by org.jmlspecs.jmldoc.jmldoc_142

Constants
Defines all additional constants shared by JML package files.

JmlAccessibleClause
An AST node class representing the JML accessible clause.

JmlAssignableClause
A JML AST node for the assignable clause.

JmlAssignmentStatement
JmlAssignmentStatement.java

JmlAxiom
This AST node represents a JML axiom annotation.

JmlBehaviorSpec
JmlBehaviorSpec.java heavyweight-spec ::= [ privacy ] "behavior" generic-spec-case

JmlCallableClause
An AST node class representing the JML callable clause.

JmlCapturesClause
An AST node class representing the JML captures clause.

JmlCodeContract
An abstraction of JML method specification.

JmlConstraint
This AST node represents a JML constraint annotation.

JmlConstructorName
This AST node represents a constructor in a JML annotation.

JmlDeclaration
This abstract class is the superclass of all jml-declaration AST nodes, (i.e., invariants, history constraints, depends declarations, and represents declarations)

JmlDivergesClause
A JML AST node class for the diverges clause.

JmlDurationClause
JmlDurationClause.java

JmlDurationExpression
JmlDurationExpression.java

JmlElemTypeExpression
JmlElemTypeExpression.java

JmlEnsuresClause
A JML AST node for the <\code>ensures clause.

JmlExample
A class representing JML example specifications.

JmlExceptionalBehaviorSpec
JmlExceptionalBehaviorSpec.java heavyweight-spec ::= [ privacy ] "exceptional_behavior" exceptional-spec-case

JmlExceptionalExample
A class representing JML exceptional example specifications.

JmlExceptionalSpecBody
An AST node class for the JML exceptional-spec-body.

JmlExpression
JmlExpression.java

JmlExtendingSpecification
A method specification that extetends inherited specifications.

JmlFieldDeclaration
JmlFieldDeclaration.java

JmlForAllVarDecl
An AST node class for the JML forall variable declarations.

JmlFreshExpression
JmlFreshExpression.java

JmlGeneralSpecCase
An abstraction of JML specification cases.

JmlGenericSpecBody
An AST node class for the JML generic-spec-body.

JmlGenericSpecCase
An AST node class for the JML generic-spec-case.

JmlGuardedStatement
JmlGuardedStatement.java

JmlHeavyweightSpec
An AST node class for the JML heavyweight-spec.

JmlInformalExpression
JmlInformalExpression.java

JmlInformalStoreRef
JmlInformalStoreRef.java

JmlInitiallyVarAssertion
This class represents a jml-var-assertion of the form initially predicate.

JmlInvariant
This AST node represents a JML invariant annotation.

JmlInvariantForExpression
AST for the JML expression \invariant_for.

JmlIsInitializedExpression
AST for the JML expression \is_initialized.

JmlLabelExpression
AST for the JML expressions \lblneg and \lblpos.

JmlLetVarDecl
An AST node class for the JML let (old) variable declarations.

JmlLockSetExpression
AST for the JML expression \lockset.

JmlMaxExpression
JmlMaxExpression.java

JmlMeasuredClause
JmlMeasuredClause.java

JmlMethodDeclaration
JmlMethodDeclaration.java

JmlMethodName
This AST node represents a method name in a JML annotation.

JmlMethodNameList
An AST node class representing the JML callable clause.

JmlMethodSpecification
An abstraction of JML method specification.

JmlModelProgram
JmlModelProgram.java

JmlMonitorsForVarAssertion
JmlMonitorsForVarAssertion.java

JmlName
This class represents a store-ref-name, store-ref-name-suffix, method-res-start, or identifier from a method-ref in an AST.

JmlNode
This is the superclass of most JML AST nodes.

JmlNondetChoiceStatement
JmlNondetChoiceStatement.java

JmlNondetIfStatement
JmlNondetIfStatement.java

JmlNonNullElementsExpression
JmlNonNullElementsExpression.java

JmlNormalBehaviorSpec
JmlNormalBehaviorSpec.java heavyweight-spec ::= [ privacy ] "normal_behavior" normal-spec-case

JmlNormalExample
A class representing JML normal example specifications.

JmlNormalSpecBody
An AST node class for the JML normal-spec-body.

JmlNotAssignedExpression
JmlNotAssignedExpression.java

JmlNotModifiedExpression
JmlNotModifiedExpression.java

JmlOldExpression
JmlOldExpression.java

JmlOnlyAssignedExpression
JmlOnlyAssignedExpression.java

JmlPredicate
This represents the AST node for a predicate in JML.

JmlPredicateClause
JmlPredicateClause.java

JmlPredicateKeyword

JmlPreExpression
JmlPreExpression.java

JmlReachExpression
An AST node class for the JML reach expressions.

JmlReadableIfVarAssertion
This class represents a jml-var-assertion of the form readable id if predicate.

JmlRedundantSpec
A class representing JML redundant specifications.

JmlRelationalExpression
This class represents the JML relational expressions.

JmlRepresentsDecl
This AST node represents a JML represents declaration annotation.

JmlRequiresClause
JmlRequiresClause.java

JmlResultExpression
JmlResultExpression.java

JmlSetComprehension
An AST node class for JML's set comprehension notation.

JmlSignalsClause
A JML AST node class for the signals clause.

JmlSignalsOnlyClause
A JML AST node class for the signals_only clause.

JmlSpaceExpression
JmlSpaceExpression.java

JmlSpecBody
JmlSpecBodyClause.java

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.

JmlSpecCase
An abstraction of JML specification cases.

JmlSpecExpression

JmlSpecification
JmlSpecification.java

JmlSpecQuantifiedExpression
An AST node class for JML quantified expressions.

JmlSpecVarDecl
An abstraction of JML specification variable declarations.

JmlStoreRef
An abstraction of JML store references.

JmlStoreRefExpression
An AST node class for JML store reference expressions.

JmlStoreRefKeyword
This class represents a JmlStoreRefKeyword in the AST.

JmlTypeDeclaration
This type represents a java class or interface in the syntax tree.

JmlTypeExpression
JmlTypeExpression.java

JmlTypeOfExpression
JmlTypeOfExpression.java

JmlVariableDefinition
A wrapper of the class JVariableDefinition to store JML-specific information.

JmlVisitor
Implementation of Visitor Design Pattern for KJC.

JmlVisitorNI
Implementation of Visitor Design Pattern for KJC.

JmlWhenClause
JmlWhenClause.java

JmlWorkingSpaceClause
JmlWorkingSpaceClause.java

JmlWorkingSpaceExpression
JmlWorkingSpaceExpression.java

JmlWritableIfVarAssertion
This class represents a jml-var-assertion of the form writable id if predicate.

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

Constants
Defines all additional constants shared by JML package files.

JmlAbruptSpecBody
JmlAbruptSpecBody.java

JmlAbruptSpecCase
JmlAbruptSpecCase.java

JmlAbstractVisitor
An abstract JML visitor class to facilitate writing concrete visitor classes that implements the interface JmlVisitor.

JmlAccessibleClause
An AST node class representing the JML accessible clause.

JmlAssertOrAssumeStatement
This class represents the type of assert-statement, and assume-statement in JML.

JmlAssertStatement
JmlAssertStatement.java

JmlAssignableClause
A JML AST node for the assignable clause.

JmlAssignmentStatement
JmlAssignmentStatement.java

JmlAssumeStatement
JmlAssumeStatement.java

JmlAxiom
This AST node represents a JML axiom annotation.

JmlBehaviorSpec
JmlBehaviorSpec.java heavyweight-spec ::= [ privacy ] "behavior" generic-spec-case

JmlBreaksClause
JmlBreaksClause.java

JmlCallableClause
An AST node class representing the JML callable clause.

JmlCapturesClause
An AST node class representing the JML captures clause.

JmlClassBlock
This class represents a instance or static initializer block annotated with a JML method specification.

JmlClassDeclaration
This type represents a java class declaration in the syntax tree.

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.

JmlCodeContract
An abstraction of JML method specification.

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

JmlCompilationUnit
This class represents a single JML compilation unit (typically a file in a file-based compiler like this) in the AST.

JmlConstraint
This AST node represents a JML constraint annotation.

JmlConstructorDeclaration
JmlConstructorDeclaration.java

JmlConstructorName
This AST node represents a constructor in a JML annotation.

JmlContinuesClause
JmlContinuesClause.java

JmlDebugStatement
A concrete AST node class to represent the debug statement of the following form: debug-statement ::= "debug" expression ;

JmlDeclaration
This abstract class is the superclass of all jml-declaration AST nodes, (i.e., invariants, history constraints, depends declarations, and represents declarations)

JMLDefaultWarningFilter
A warning filter for JML.

JmlDivergesClause
A JML AST node class for the diverges clause.

JmlDurationClause
JmlDurationClause.java

JmlDurationExpression
JmlDurationExpression.java

JmlElemTypeExpression
JmlElemTypeExpression.java

JmlEnsuresClause
A JML AST node for the <\code>ensures clause.

JmlExample
A class representing JML example specifications.

JmlExceptionalBehaviorSpec
JmlExceptionalBehaviorSpec.java heavyweight-spec ::= [ privacy ] "exceptional_behavior" exceptional-spec-case

JmlExceptionalExample
A class representing JML exceptional example specifications.

JmlExceptionalSpecBody
An AST node class for the JML exceptional-spec-body.

JmlExceptionalSpecCase
An AST node class for the JML exceptional-spec-case.

JmlExpression
JmlExpression.java

JmlExtendingSpecification
A method specification that extetends inherited specifications.

JmlFieldDeclaration
JmlFieldDeclaration.java

JmlForAllVarDecl
An AST node class for the JML forall variable declarations.

JmlFormalParameter
This class represents a formal parameter in a JML AST.

JmlFreshExpression
JmlFreshExpression.java

JmlGeneralSpecCase
An abstraction of JML specification cases.

JmlGenericSpecBody
An AST node class for the JML generic-spec-body.

JmlGenericSpecCase
An AST node class for the JML generic-spec-case.

JmlGuardedStatement
JmlGuardedStatement.java

JmlHeavyweightSpec
An AST node class for the JML heavyweight-spec.

JmlHenceByStatement
JmlHenceByStatement.java

JmlInformalExpression
JmlInformalExpression.java

JmlInformalStoreRef
JmlInformalStoreRef.java

JmlInGroupClause
This class represents a jml-var-assertion of the form initially predicate.

JmlInitiallyVarAssertion
This class represents a jml-var-assertion of the form initially predicate.

JmlInterfaceDeclaration
This class represents a java interface in the syntax tree

JmlInvariant
This AST node represents a JML invariant annotation.

JmlInvariantForExpression
AST for the JML expression \invariant_for.

JmlInvariantStatement
JmlInvariantStatement.java

JmlIsInitializedExpression
AST for the JML expression \is_initialized.

JmlLabelExpression
AST for the JML expressions \lblneg and \lblpos.

JmlLetVarDecl
An AST node class for the JML let (old) variable declarations.

JmlLockSetExpression
AST for the JML expression \lockset.

JmlLoopInvariant
JmlLoopInvariant.java

JmlLoopSpecification
This is the super class for the classes representing loop-invariant and variant-function annotations for loop-stmt.

JmlLoopStatement
This class represents loop-stmts annotated with loop-invariants and/or variant-functions.

JmlMapsIntoClause
This class represents a jml-var-assertion of the form initially predicate.

JmlMaxExpression
JmlMaxExpression.java

JmlMeasuredClause
JmlMeasuredClause.java

JmlMemberDeclaration
This type represents a java declaration in the syntax tree.

JmlMethodDeclaration
JmlMethodDeclaration.java

JmlMethodName
This AST node represents a method name in a JML annotation.

JmlMethodNameList
An AST node class representing the JML callable clause.

JmlMethodSpecification
An abstraction of JML method specification.

JmlModelProgram
JmlModelProgram.java

JmlMonitorsForVarAssertion
JmlMonitorsForVarAssertion.java

JmlName
This class represents a store-ref-name, store-ref-name-suffix, method-res-start, or identifier from a method-ref in an AST.

JmlNode
This is the superclass of most JML AST nodes.

JmlNondetChoiceStatement
JmlNondetChoiceStatement.java

JmlNondetIfStatement
JmlNondetIfStatement.java

JmlNonNullElementsExpression
JmlNonNullElementsExpression.java

JmlNormalBehaviorSpec
JmlNormalBehaviorSpec.java heavyweight-spec ::= [ privacy ] "normal_behavior" normal-spec-case

JmlNormalExample
A class representing JML normal example specifications.

JmlNormalSpecBody
An AST node class for the JML normal-spec-body.

JmlNormalSpecCase
An AST node class for the JML normal-spec-case.

JmlNotAssignedExpression
JmlNotAssignedExpression.java

JmlNotModifiedExpression
JmlNotModifiedExpression.java

JmlOldExpression
JmlOldExpression.java

JmlOnlyAccessedExpression
JmlOnlyAccessedExpression.java

JmlOnlyAssignedExpression
JmlOnlyAssignedExpression.java

JmlOnlyCalledExpression
JmlOnlyCalledExpression.java

JmlOnlyCapturedExpression
JmlOnlyCapturedExpression.java

JmlPackageImport
This type represents (in the AST) full-package import statements.

JmlPredicate
This represents the AST node for a predicate in JML.

JmlPredicateClause
JmlPredicateClause.java

JmlPredicateKeyword

JmlPreExpression
JmlPreExpression.java

JmlReachExpression
An AST node class for the JML reach expressions.

JmlReadableIfVarAssertion
This class represents a jml-var-assertion of the form readable id if predicate.

JmlRedundantSpec
A class representing JML redundant specifications.

JmlRefinePrefix

JmlRelationalExpression
This class represents the JML relational expressions.

JmlRepresentsDecl
This AST node represents a JML represents declaration annotation.

JmlRequiresClause
JmlRequiresClause.java

JmlResultExpression
JmlResultExpression.java

JmlReturnsClause
JmlReturnsClause.java

JmlSetComprehension
An AST node class for JML's set comprehension notation.

JmlSetStatement
JmlSetStatement.java

JmlSignalsClause
A JML AST node class for the signals clause.

JmlSignalsOnlyClause
A JML AST node class for the signals_only clause.

JmlSourceField
A class for representing an exported field of a class.

JmlSpaceExpression
JmlSpaceExpression.java

JmlSpecBody
JmlSpecBodyClause.java

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.

JmlSpecCase
An abstraction of JML specification cases.

JmlSpecExpression

JmlSpecExpressionWrapper
This abstract class is the super class of all JmlExpressions that simply modify a spec-expression (e.g.

JmlSpecification
JmlSpecification.java

JmlSpecQuantifiedExpression
An AST node class for JML quantified expressions.

JmlSpecStatement
JmlSpecStatement.java

JmlSpecVarDecl
An abstraction of JML specification variable declarations.

JmlStoreRef
An abstraction of JML store references.

JmlStoreRefExpression
An AST node class for JML store reference expressions.

JmlStoreRefKeyword
This class represents a JmlStoreRefKeyword in the AST.

JmlStoreRefListWrapper
JmlStoreRefListWrapper.java

JmlTypeDeclaration
This type represents a java class or interface in the syntax tree.

JmlTypeExpression
JmlTypeExpression.java

JmlTypeOfExpression
JmlTypeOfExpression.java

JmlUnreachableStatement
JmlUnreachableStatement.java

JmlVariableDefinition
A wrapper of the class JVariableDefinition to store JML-specific information.

JmlVariantFunction
JmlVariantFunction.java

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

JmlVisitor
Implementation of Visitor Design Pattern for KJC.

JMLWarningFilter
A warning filter for JML.

JmlWhenClause
JmlWhenClause.java

JmlWorkingSpaceClause
JmlWorkingSpaceClause.java

JmlWorkingSpaceExpression
JmlWorkingSpaceExpression.java

JmlWritableIfVarAssertion
This class represents a jml-var-assertion of the form writable id if predicate.

Main
This class implements the entry point of the JML compiler.

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

Constants
Defines all additional constants shared by JML package files.

JmlAbstractVisitor
An abstract JML visitor class to facilitate writing concrete visitor classes that implements the interface JmlVisitor.

JmlDurationExpression
JmlDurationExpression.java

JmlElemTypeExpression
JmlElemTypeExpression.java

JmlFreshExpression
JmlFreshExpression.java

JmlInformalExpression
JmlInformalExpression.java

JmlInvariantForExpression
AST for the JML expression \invariant_for.

JmlIsInitializedExpression
AST for the JML expression \is_initialized.

JmlLabelExpression
AST for the JML expressions \lblneg and \lblpos.

JmlLockSetExpression
AST for the JML expression \lockset.

JmlMaxExpression
JmlMaxExpression.java

JmlNonNullElementsExpression
JmlNonNullElementsExpression.java

JmlOldExpression
JmlOldExpression.java

JmlPredicate
This represents the AST node for a predicate in JML.

JmlPreExpression
JmlPreExpression.java

JmlReachExpression
An AST node class for the JML reach expressions.

JmlRelationalExpression
This class represents the JML relational expressions.

JmlResultExpression
JmlResultExpression.java

JmlSetComprehension
An AST node class for JML's set comprehension notation.

JmlSpaceExpression
JmlSpaceExpression.java

JmlSpecExpression

JmlSpecQuantifiedExpression
An AST node class for JML quantified expressions.

JmlTypeExpression
JmlTypeExpression.java

JmlTypeOfExpression
JmlTypeOfExpression.java

JmlVisitor
Implementation of Visitor Design Pattern for KJC.

JmlWorkingSpaceExpression
JmlWorkingSpaceExpression.java

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

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

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

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

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

Constants
Defines all additional constants shared by JML package files.

JmlClassDeclaration
This type represents a java class declaration in the syntax tree.

JmlCompilationUnit
This class represents a single JML compilation unit (typically a file in a file-based compiler like this) in the AST.

JmlConstructorDeclaration
JmlConstructorDeclaration.java

JmlFieldDeclaration
JmlFieldDeclaration.java

JmlMethodDeclaration
JmlMethodDeclaration.java

JmlTypeDeclaration
This type represents a java class or interface in the syntax tree.

JmlVisitor
Implementation of Visitor Design Pattern for KJC.