JML

Uses of Interface
org.multijava.util.compiler.PhylumType

Packages that use PhylumType
org.jmlspecs.checker Contains the source code for a parser and typechecker for JML annotations and java code. 
org.jmlspecs.jmlrac Generates Java classes from JML specifications that check assertions at runtime. 
org.multijava.mjc Implements mjc, a MultiJava compiler. 
org.multijava.util.compiler Provides utilities and superclasses for the compilers in MultiJava and the Java Modeling Language
 

Uses of PhylumType in org.jmlspecs.checker
 

Classes in org.jmlspecs.checker that implement PhylumType
 class JClassDeclarationWrapper
          A wrapper class to JClassDeclaration to implement JML-specific typechecking.
 class JConstructorBlockWrapper
           
 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 JmlAccessibleClause
          An AST node class representing the JML accessible clause.
 class JmlAddExpression
          This class represents the addition binary expression.
 class JmlArrayDimsAndInits
          JmlArrayDimsAndInits.java
 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 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 JmlBinaryType
          This class represents a class read from a *.class file.
 class JmlBitwiseExpression
          This class represents the addition binary expression.
 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 JmlCastExpression
          JmlCastExpression.java This class represents a cast expression such as /*@(non_null)* / o /*@(non_null T)* / o (/*@non_null* / T) o
 class JmlClassBlock
          This class represents a instance or static initializer block annotated with a JML method specification.
 class JmlClassDeclaration
          This type represents a java class declaration in the syntax tree.
 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 JmlConstraint
          This AST node represents a JML constraint annotation.
 class JmlConstructorDeclaration
          JmlConstructorDeclaration.java
 class JmlConstructorName
          This AST node represents a constructor in a JML annotation.
 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 JmlDivideExpression
          This class represents the addition binary expression.
 class JmlDurationClause
          JmlDurationClause.java
 class JmlDurationExpression
          JmlDurationExpression.java
 class JmlElemTypeExpression
          JmlElemTypeExpression.java
 class JmlEnsuresClause
          A JML AST node for the <\code>ensures clause.
 class JmlEqualityExpression
          This class represents the AST node for the equality operators.
 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 JmlExtendingSpecification
          A method specification that extetends inherited specifications.
 class JmlFieldDeclaration
          JmlFieldDeclaration.java
 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 JmlGuardedStatement
          JmlGuardedStatement.java
 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 JmlInitiallyVarAssertion
          This class represents a jml-var-assertion of the form initially predicate.
 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 JmlInvariantStatement
          JmlInvariantStatement.java
 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 JmlMemberDeclaration
          This type represents a java declaration in the syntax tree.
 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 JmlMinusExpression
          This class represents the addition binary expression.
 class JmlModelProgram
          JmlModelProgram.java
 class JmlModelProgStatement
          The type of model-prog-statements.
 class JmlModuloExpression
          This class represents the addition binary expression.
 class JmlMonitorsForVarAssertion
          JmlMonitorsForVarAssertion.java
 class JmlMultExpression
          This class represents the addition binary expression.
 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.
(package private) static class JmlNode.DummyInitializerDeclaration
          A class for dummy initializer declarations.
 class JmlNondetChoiceStatement
          JmlNondetChoiceStatement.java
 class JmlNondetIfStatement
          JmlNondetIfStatement.java
 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 JmlOldExpression
          JmlOldExpression.java
 class JmlOnlyAccessedExpression
          JmlOnlyAccessedExpression.java
 class JmlOnlyAssignedExpression
          JmlOnlyAssignedExpression.java
 class JmlOnlyCalledExpression
          JmlOnlyCalledExpression.java
 class JmlOnlyCapturedExpression
          JmlOnlyCapturedExpression.java
 class JmlOrdinalLiteral
          This class represents jml specific ordinal literals (bigint)
 class JmlPackageImport
          This type represents (in the AST) full-package import statements.
 class JmlPredicate
          This represents the AST node for a predicate in JML.
 class JmlPredicateClause
          JmlPredicateClause.java
 class JmlPredicateKeyword
           
 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 JmlShiftExpression
          This class represents the addition binary expression.
 class JmlSignalsClause
          A JML AST node class for the signals clause.
 class JmlSignalsOnlyClause
          A JML AST node class for the signals_only clause.
 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 JmlSpecExpression
           
 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 JmlSpecStatement
          JmlSpecStatement.java
 class JmlSpecStatementClause
          JmlSpecStatementClause.java
 class JmlSpecVarDecl
          An abstraction of JML specification variable declarations.
 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 JmlUnreachableStatement
          JmlUnreachableStatement.java
 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.
 

Uses of PhylumType in org.jmlspecs.jmlrac
 

Classes in org.jmlspecs.jmlrac that implement PhylumType
static class RacParser.RacBlock
          A RAC node class for representing blocks.
static class RacParser.RacMethodDeclaration
          A RAC node class for representing method declarations.
static class RacParser.RacStatement
          A RAC node class for representing statements.
 class RacPredicate
          An AST node class for RAC-specific predicates.
(package private)  class TransInvariant.CallExpr
           
(package private)  class TransInvariant.CallExpr2
           
 

Uses of PhylumType in org.multijava.mjc
 

Subinterfaces of PhylumType in org.multijava.mjc
 interface JClassDeclarationType
          This type represents a java class declaration in the syntax tree.
 interface JConstructorDeclarationType
          This type represents a constructor in the AST.
 interface JFieldDeclarationType
          This type represents a field declaration in the syntax tree.
 interface JInterfaceDeclarationType
          This type represents a java interface in the syntax tree.
 interface JMemberDeclarationType
          This type represents a java declaration in the syntax tree.
 interface JMethodDeclarationType
          This type represents a java method in the syntax tree.
 interface JTypeDeclarationType
          This type represents a java class or interface in the syntax tree
 

Classes in org.multijava.mjc that implement PhylumType
(package private)  class CCORInitializer.CCORInitializer$1
           
(package private)  class CSourceClass.CSourceClass$1
           
(package private)  class CSourceDispatcherClass.CSourceDispatcherClass$2
           
 class JAddExpression
          This class represents the addition binary expression.
 class JArrayAccessExpression
          This class implements an access to an array.
 class JArrayDimsAndInits
          This class implements an AST node representing a list of expressions used in array dimensioning and an array initialization expression, as in the [1][2][3] in new Integer[1][2][3] or the { 1, 2, 3 } in Integer[] foo = { 1, 2, 3 }.
 class JArrayInitializer
          This class implements a constant list of expressions used in array initialisation.
 class JArrayLengthExpression
          This class represents an array length expression in the AST.
 class JAssertStatement
          The syntax for Java assert statements is defined as follows.
 class JAssignmentExpression
          This class implements the assignment operation
 class JBinaryArithmeticExpression
          This class is an abstract root class for binary expressions.
 class JBinaryExpression
          This class is an abstract root class for binary expressions Here are conversion method following JLS 5.6.2
 class JBitwiseExpression
          This class represents the bitwise AND, OR, and XOR binary expressions.
 class JBlock
          A block is a sequence of statements and local variable declaration statements within braces.
 class JBooleanLiteral
          Root class for all expressions
 class JBreakStatement
          This class represents a break statement.
 class JCastExpression
          This class represents a cast expression '((byte)2)'
 class JCatchClause
          This class represents a catch clause in the syntax tree.
 class JCharLiteral
          A simple character constant
 class JCheckedExpression
          This AST node is used to add a portion of already checked code into code that needs to be checked.
 class JClassBlock
          This class represents an initializer block in a type declaration.
 class JClassDeclaration
          This class represents a java class in the syntax tree
 class JClassExpression
          This class represents an AST node for a class literal expression, e.g., int.class and String.class.
 class JClassFieldDeclarator
          JLS 14.5: Field Statement.
 class JClassFieldExpression
          This class represents the AST node for a field access, e.g.
 class JClassOrGFImport
          This class 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 JCompilationUnit
          This class represents a single Java compilation unit (typically a file in a file-based compiler like this) in the AST.
 class JCompoundAssignmentExpression
          This class represents the compound assignment operation, e.g., x += 3 and y *= 4, in the AST.
 class JCompoundStatement
          A compound statement is a sequence of statements and local variable declaration statements without braces.
 class JConditionalAndExpression
          This class implements the conditional and operation
 class JConditionalExpression
          This class implements expressions using the conditional operator.
 class JConditionalOrExpression
          This class implements the conditional or operation
 class JConstructorBlock
          This class represents the block of a constructor.
 class JConstructorDeclaration
          This class represents a constructor in the AST
 class JContinueStatement
          A continue statement may occur only in a while, do, or for statement; statements of these three kinds are called iteration statements.
 class JDivideExpression
          This class represents the division binary expression.
 class JDoStatement
          This class represents a do statement in the AST.
 class JEmptyStatement
          This class represents an empty statement, which does nothing.
 class JEqualityExpression
          This class represents the AST node for the equality operators.
 class JExplicitConstructorInvocation
          This class represents a explicit call to a super or self constructor.
 class JExpression
          This class is the root class for all classes representing expression nodes in the AST.
 class JExpressionListStatement
          This class represents an expression list, a comma-separated list of expression statements used in the initializer and iterator of a for-loop statement.
 class JExpressionStatement
          Certain kinds of expressions may be used as statements by following them with semicolon.
 class JFieldDeclaration
          This class represents a field declaration in the syntax tree.
 class JFormalParameter
          This class represents a parameter declaration in the syntax tree
 class JForStatement
          This class represents a for statement in the AST.
 class JGeneratedLocalVariable
          This class represents a compiler-generated local variable declaration.
 class JIfStatement
          This class represents an if statement in the AST.
 class JInitializerDeclaration
          This class represents an initializer (either static or instance) in the AST.
 class JInstanceofExpression
          This class represents an instanceof expression.
 class JInterfaceDeclaration
          This class represents a java interface in the syntax tree
 class JLabeledStatement
          This class represents a labeled statement.
 class JLiteral
          Root class for all literals expression
 class JLocalVariable
          This class represents a local variable declaration in the AST.
 class JLocalVariableExpression
          This class represents the AST node for local variable references.
 class JLoopStatement
          This abstract class is the superclass for all the classes representing loop statements in the AST.
 class JMemberDeclaration
          This class represents a java declaration in the syntax tree
 class JMethodCallExpression
          This class represents method calls methodname( e1, e2, ..., en )
 class JMethodDeclaration
          This class represents a java method in the syntax tree.
(package private)  class JMethodDeclaration.JMethodDeclaration$1
           
 class JMinusExpression
          This class represents the subtraction binary expression.
 class JModuloExpression
          This class represents the modulo binary expression.
 class JMultExpression
          This class represents the multiplication binary expression.
 class JNameExpression
          This class represents a name within an expression.
 class JNewAnonymousClassExpression
          This class represents a new anonymous class allocation expression.
 class JNewArrayExpression
          This class represents a new array allocation expression 'new type[...]'
 class JNewObjectExpression
          This class represents an object instantiation expression 'new type(...)'
 class JNullLiteral
          A simple character constant
 class JNumberLiteral
          Root class for all number literals
 class JOrdinalLiteral
          This class represents literals of primitive integral types (byte, short, int, long).
 class JOuterLocalVariableExpression
          This class is an AST node and represents a reference to a variable of a surrounding lexical context from within an inner class.
 class JPackageImport
          This class represents (in the AST) full-package import statements, an asterisk.
 class JPackageName
          This class represents package statements in the AST, like package org.multijava.mjc.
 class JParenthesedExpression
          This class represents expression within parentheses.
 class JPhylum
          This class is a superclass for all elements of the parsing tree.
 class JPostfixExpression
          This class represents postfix increment and decrement expressions.
 class JPrefixExpression
          This class represents prefix increment and decrement expressions.
 class JRealLiteral
          This class represents real-valued literals (float, double)
 class JRelationalExpression
          This class represents the AST node for the relational operators, <, >, etc.
 class JResendExpression
          This class represents a MultiJava resend expression, for invoking a directly overridden method of the caller's generic function.
 class JReturnStatement
          This class represents a return statement in the AST.
 class JShiftExpression
          This class represents the shift (left, right, boolean-right) binary expressions.
 class JStatement
          This class is the root class for all classes representing statement nodes in the AST.
 class JStringLiteral
          A simple character constant
 class JSuperExpression
          This class represents a "super" primary expression in an AST.
 class JSwitchGroup
          This class represents an AST node for a group in a switch statement.
 class JSwitchLabel
          This class represents an AST node for the label for a single case of a switch statement.
 class JSwitchStatement
          This class represents a switch statement in the AST.
 class JSynchronizedStatement
          This class represents a synchronized statement in an AST.
 class JThisExpression
          A 'this' expression
(package private)  class JThisExpression.JThisExpression$1
           
(package private)  class JThisExpression.JThisExpression$2
           
 class JThrowStatement
          This class represents a throw statement in the AST.
 class JTryCatchStatement
          This class represents a try-catch statement in the AST.
 class JTryFinallyStatement
          This class represents a try-catch statement in the AST.
 class JTypeDeclaration
          This class represents a java class or interface in the syntax tree
 class JTypeDeclarationStatement
          This class represents a local type declaration statement.
 class JTypeNameExpression
          This class represents the AST node for a type name expression like Object
 class JUnaryExpression
          This class represents unary expressions (unary plus, unary minus, bitwise complement, and logical not).
 class JUnaryPromote
          This class promotes an arithmetic expression to a new type.
 class JVariableDeclarationStatement
          A local variable declaration statement declares one or more local variable names.
 class JVariableDefinition
          This class represents a local variable definition in the syntax tree.
 class JWhileStatement
          This class represents a while statement in the AST.
 class MJGenericFunctionDecl
          This class represents a group of method declarations, all sharing the same name, that together form the top of one or more overloaded external generic function lattices.
 class MJMathModeExpression
          This AST node is used to change the arithmetic mode for a given expression.
 class MJTopLevelAbstractMethodDeclaration
           
 class MJTopLevelMethodDeclaration
           
 class MJWarnExpression
          This AST node is used to enable or disable the compile-time and run-time checking of integral arithmetic overflow.
 

Uses of PhylumType in org.multijava.util.compiler
 

Classes in org.multijava.util.compiler that implement PhylumType
 class Phylum
          This class represents the root class for all elements of the parsing tree
 


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.