Overview   Package  Class  Use  Tree  Deprecated  Index  Help 
JML
 PREV PACKAGE   NEXT PACKAGE FRAMES    NO FRAMES    

Package org.jmlspecs.checker

Contains the source code for a parser and typechecker for JML annotations and java code.

See:
          Description

Interface Summary
Constants Defines all additional constants shared by JML package files.
JavadocJmlLexerTokenTypes  
JavadocJmlTokenTypes  
JmlAnnotatable This interface is implemented by AST nodes that can have child nodes that represent JML annotations.
JmlExprIDTokenTypes  
JmlIDTokenTypes  
JmlJDLexerTokenTypes  
JmlLexerTokenTypes  
JmlMLLexerTokenTypes  
JmlSLLexerTokenTypes  
JmlTokenTypes  
JmlTopIDTokenTypes  
JmlVisitor Implementation of Visitor Design Pattern for KJC.
 

Class Summary
AndNotPatternFilenameFilter Decorates the file name filter given to the constructor so it does not match names that include the pattern given to the constructor.
CParseClassContext This class is used by the parser to collect the members of a class declaration.
CTypeType This class represents the JML \TYPE type.
JavadocJmlLexer  
JavadocJmlParser  
JClassDeclarationWrapper A wrapper class to JClassDeclaration to implement JML-specific typechecking.
JConstructorBlockWrapper  
JConstructorDeclarationWrapper A class representing a constructor declaration in the syntax tree.
JFieldDeclarationWrapper A class representing a field declaration in the syntax tree.
JInterfaceDeclarationWrapper This class represents a java interface in the syntax tree
JMethodDeclarationWrapper A class representing a method declaration 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.
JmlAccumSubclassingInfo  
JmlAddExpression This class represents the addition binary expression.
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
JmlBinaryArithmeticExpressionHelper This class is an abstract root class for binary expressions.
JmlBinaryField This class represents a class read from a *.class file.
JmlBinaryMember This type represents a java declaration in the syntax tree.
JmlBinaryMethod This class represents a method read from a *.class file.
JmlBinarySourceClass This class represents a class read from a *.class file.
JmlBinaryType This class represents a class read from a *.class file.
JmlBitwiseExpression This class represents the addition binary expression.
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.
JmlCompilationUnitContext This class represents the context for a compilation unit during checking passes (checkInterface, checkInitializers, typecheck).
JmlConstraint This AST node represents a JML constraint annotation.
JmlConstructorContext This class represents the context for a constructor during checking passes (checkInterface, checkInitializers, typecheck).
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)
JMLDefaultWarningFilter A warning filter for JML.
JmlDivergesClause A JML AST node class for the diverges clause.
JmlDivideExpression This class represents the addition binary expression.
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
JmlExpressionChecker A visitor class to check privacy (and purity) of JML expressions.
JmlExpressionContext A class for representing the context in which JML expressions are typechecked.
JmlExpressionFactory Expression AST node factory class.
JmlExprIDKeywords  
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.
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).
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
JmlIDKeywords  
JmlInformalExpression JmlInformalExpression.java
JmlInformalStoreRef JmlInformalStoreRef.java
JmlInGroupClause This class represents a jml-var-assertion of the form initially predicate.
JmlInitializerContext This class represents the context for a static initializer during checking passes (checkInterface, checkInitializers, typecheck).
JmlInitiallyVarAssertion This class represents a jml-var-assertion of the form initially predicate.
JmlInterfaceContext This class represents the context for an interface declaration during checking passes (checkInterface, checkInitializers, typecheck).
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.
JmlJDLexer This is the scanner for embedded JML annotations.
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.
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.
JmlMessages  
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.
JmlMinusExpression This class represents the addition binary expression.
JmlMLLexer This is the scanner for multi-line JML annotations.
JmlModelProgram JmlModelProgram.java
JmlModelProgStatement The type of model-prog-statements.
JmlModuloExpression This class represents the addition binary expression.
JmlMonitorsForVarAssertion JmlMonitorsForVarAssertion.java
JmlMultExpression This class represents the addition binary expression.
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.
JmlNode.DummyInitializerDeclaration A class for dummy initializer declarations.
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.
JmlOrdinalLiteral This class represents jml specific ordinal literals (bigint)
JmlOtherRef An AST node class representing JML references to an arbitrary object.
JmlPackageImport This type represents (in the AST) full-package import statements.
JmlParser  
JmlParser.StringBooleanPair  
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.
JmlParserUtility This class is derived from ...mjc.ParserUtility; its purpose is to supply a different JavadocParser than the one in org.multijava.mjc.
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
JmlShiftExpression This class represents the addition binary expression.
JmlSigBinaryClass A class to represent JML class declaratons read from bytecode files.
JmlSigBinaryField A class to represent JML field declaratons read from bytecode files.
JmlSigBinaryMethod A class to represent JML method declaratons read from bytecode files.
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  
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.
JmlStdType This class is a singleton that provides variables for the various built-in and java.lang types.
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
JmlTopIDKeywords  
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
JmlUnaryExpression This class represents unary expressions (unary plus, unary minus, bitwise complement, and logical not).
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.
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.Filter This class is used with the Directory.list method to list those files in a directory that this program is interested in processing - in this case, all those that end in '.java', '.jml' or '.spec'.
Main.PTMode  
NonNullStatistics  
TestJmlParser Unit tests for JmlParser
TestJmlParser.Helper  
TestSuite This class is automatically generated using org.multijava.util.testing.Main and is used to group a collection of JUnit tests for the local package and perhaps some subpackages.
TestSuite.TestSuite$1  
TokenStreamSelector Provides for switching between various lexical analyzers for lexing JML.
 

Package org.jmlspecs.checker Description

Contains the source code for a parser and typechecker for JML annotations and java code. The package serves also as a basis for deriving other tools operating jml and java parse trees.

Related Documentation

For an overview, syntax, informal semantics, and examples of the JML language, please refer to:

Overview   Package  Class  Use  Tree  Deprecated  Index  Help 
JML
 PREV PACKAGE   NEXT PACKAGE FRAMES    NO FRAMES    
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.