JML

org.jmlspecs.checker
Interface JmlVisitor

All Superinterfaces:
MjcVisitor
All Known Subinterfaces:
RacVisitor
All Known Implementing Classes:
DesugarSpec, JmlAbstractVisitor, JmlRacGenerator, JmlVisitorNI, RacAbstractVisitor, RacPrettyPrinter, TransMethod.SpecCaseCollector

public interface JmlVisitor
extends MjcVisitor

Implementation of Visitor Design Pattern for KJC. Suggested from: Max R. Andersen(max@cs.auc.dk) !CONVERT! use open classes


Method Summary
 void visitJmlAbruptSpecBody(JmlAbruptSpecBody self)
           
 void visitJmlAbruptSpecCase(JmlAbruptSpecCase self)
           
 void visitJmlAccessibleClause(JmlAccessibleClause self)
           
 void visitJmlAssertStatement(JmlAssertStatement self)
           
 void visitJmlAssignableClause(JmlAssignableClause self)
           
 void visitJmlAssignmentStatement(JmlAssignmentStatement self)
           
 void visitJmlAssumeStatement(JmlAssumeStatement self)
           
 void visitJmlAxiom(JmlAxiom self)
           
 void visitJmlBehaviorSpec(JmlBehaviorSpec self)
           
 void visitJmlBreaksClause(JmlBreaksClause self)
           
 void visitJmlCallableClause(JmlCallableClause self)
           
 void visitJmlCapturesClause(JmlCapturesClause self)
           
 void visitJmlClassBlock(JmlClassBlock self)
           
 void visitJmlClassDeclaration(JmlClassDeclaration self)
           
 void visitJmlClassOrGFImport(JmlClassOrGFImport self)
           
 void visitJmlCodeContract(JmlCodeContract self)
           
 void visitJmlCompilationUnit(JmlCompilationUnit self)
           
 void visitJmlConstraint(JmlConstraint self)
           
 void visitJmlConstructorDeclaration(JmlConstructorDeclaration self)
           
 void visitJmlConstructorName(JmlConstructorName self)
           
 void visitJmlContinuesClause(JmlContinuesClause self)
           
 void visitJmlDebugStatement(JmlDebugStatement self)
           
 void visitJmlDeclaration(JmlDeclaration self)
           
 void visitJmlDivergesClause(JmlDivergesClause self)
           
 void visitJmlDurationClause(JmlDurationClause self)
           
 void visitJmlDurationExpression(JmlDurationExpression self)
           
 void visitJmlElemTypeExpression(JmlElemTypeExpression self)
           
 void visitJmlEnsuresClause(JmlEnsuresClause self)
           
 void visitJmlExample(JmlExample self)
           
 void visitJmlExceptionalBehaviorSpec(JmlExceptionalBehaviorSpec self)
           
 void visitJmlExceptionalExample(JmlExceptionalExample self)
           
 void visitJmlExceptionalSpecBody(JmlExceptionalSpecBody self)
           
 void visitJmlExceptionalSpecCase(JmlExceptionalSpecCase self)
           
 void visitJmlExpression(JmlExpression self)
           
 void visitJmlExtendingSpecification(JmlExtendingSpecification self)
           
 void visitJmlFieldDeclaration(JmlFieldDeclaration self)
           
 void visitJmlForAllVarDecl(JmlForAllVarDecl self)
           
 void visitJmlFormalParameter(JmlFormalParameter self)
           
 void visitJmlFreshExpression(JmlFreshExpression self)
           
 void visitJmlGeneralSpecCase(JmlGeneralSpecCase self)
           
 void visitJmlGenericSpecBody(JmlGenericSpecBody self)
           
 void visitJmlGenericSpecCase(JmlGenericSpecCase self)
           
 void visitJmlGuardedStatement(JmlGuardedStatement self)
           
 void visitJmlHenceByStatement(JmlHenceByStatement self)
           
 void visitJmlInformalExpression(JmlInformalExpression self)
           
 void visitJmlInformalStoreRef(JmlInformalStoreRef self)
           
 void visitJmlInGroupClause(JmlInGroupClause self)
           
 void visitJmlInitiallyVarAssertion(JmlInitiallyVarAssertion self)
           
 void visitJmlInterfaceDeclaration(JmlInterfaceDeclaration self)
           
 void visitJmlInvariant(JmlInvariant self)
           
 void visitJmlInvariantForExpression(JmlInvariantForExpression self)
           
 void visitJmlInvariantStatement(JmlInvariantStatement self)
           
 void visitJmlIsInitializedExpression(JmlIsInitializedExpression self)
           
 void visitJmlLabelExpression(JmlLabelExpression self)
           
 void visitJmlLetVarDecl(JmlLetVarDecl self)
           
 void visitJmlLockSetExpression(JmlLockSetExpression self)
           
 void visitJmlLoopInvariant(JmlLoopInvariant self)
           
 void visitJmlLoopStatement(JmlLoopStatement self)
           
 void visitJmlMapsIntoClause(JmlMapsIntoClause self)
           
 void visitJmlMaxExpression(JmlMaxExpression self)
           
 void visitJmlMeasuredClause(JmlMeasuredClause self)
           
 void visitJmlMethodDeclaration(JmlMethodDeclaration self)
           
 void visitJmlMethodName(JmlMethodName self)
           
 void visitJmlMethodNameList(JmlMethodNameList self)
           
 void visitJmlMethodSpecification(JmlMethodSpecification self)
           
 void visitJmlModelProgram(JmlModelProgram self)
           
 void visitJmlMonitorsForVarAssertion(JmlMonitorsForVarAssertion self)
           
 void visitJmlName(JmlName self)
           
 void visitJmlNode(JmlNode self)
           
 void visitJmlNondetChoiceStatement(JmlNondetChoiceStatement self)
           
 void visitJmlNondetIfStatement(JmlNondetIfStatement self)
           
 void visitJmlNonNullElementsExpression(JmlNonNullElementsExpression self)
           
 void visitJmlNormalBehaviorSpec(JmlNormalBehaviorSpec self)
           
 void visitJmlNormalExample(JmlNormalExample self)
           
 void visitJmlNormalSpecBody(JmlNormalSpecBody self)
           
 void visitJmlNormalSpecCase(JmlNormalSpecCase self)
           
 void visitJmlNotAssignedExpression(JmlNotAssignedExpression self)
           
 void visitJmlNotModifiedExpression(JmlNotModifiedExpression self)
           
 void visitJmlOldExpression(JmlOldExpression self)
           
 void visitJmlOnlyAccessedExpression(JmlOnlyAccessedExpression self)
           
 void visitJmlOnlyAssignedExpression(JmlOnlyAssignedExpression self)
           
 void visitJmlOnlyCalledExpression(JmlOnlyCalledExpression self)
           
 void visitJmlOnlyCapturedExpression(JmlOnlyCapturedExpression self)
           
 void visitJmlPackageImport(JmlPackageImport self)
           
 void visitJmlPredicate(JmlPredicate self)
           
 void visitJmlPredicateKeyword(JmlPredicateKeyword self)
           
 void visitJmlPreExpression(JmlPreExpression self)
           
 void visitJmlReachExpression(JmlReachExpression self)
           
 void visitJmlReadableIfVarAssertion(JmlReadableIfVarAssertion self)
           
 void visitJmlRedundantSpec(JmlRedundantSpec self)
           
 void visitJmlRefinePrefix(JmlRefinePrefix self)
           
 void visitJmlRelationalExpression(JmlRelationalExpression self)
           
 void visitJmlRepresentsDecl(JmlRepresentsDecl self)
           
 void visitJmlRequiresClause(JmlRequiresClause self)
           
 void visitJmlResultExpression(JmlResultExpression self)
           
 void visitJmlReturnsClause(JmlReturnsClause self)
           
 void visitJmlSetComprehension(JmlSetComprehension self)
           
 void visitJmlSetStatement(JmlSetStatement self)
           
 void visitJmlSignalsClause(JmlSignalsClause self)
           
 void visitJmlSignalsOnlyClause(JmlSignalsOnlyClause self)
           
 void visitJmlSpaceExpression(JmlSpaceExpression self)
           
 void visitJmlSpecBody(JmlSpecBody self)
           
 void visitJmlSpecExpression(JmlSpecExpression self)
           
 void visitJmlSpecification(JmlSpecification self)
           
 void visitJmlSpecQuantifiedExpression(JmlSpecQuantifiedExpression self)
           
 void visitJmlSpecStatement(JmlSpecStatement self)
           
 void visitJmlSpecVarDecl(JmlSpecVarDecl self)
           
 void visitJmlStoreRef(JmlStoreRef self)
           
 void visitJmlStoreRefExpression(JmlStoreRefExpression self)
           
 void visitJmlStoreRefKeyword(JmlStoreRefKeyword self)
           
 void visitJmlTypeExpression(JmlTypeExpression self)
           
 void visitJmlTypeOfExpression(JmlTypeOfExpression self)
           
 void visitJmlUnreachableStatement(JmlUnreachableStatement self)
           
 void visitJmlVariableDefinition(JmlVariableDefinition self)
           
 void visitJmlVariantFunction(JmlVariantFunction self)
           
 void visitJmlWhenClause(JmlWhenClause self)
           
 void visitJmlWorkingSpaceClause(JmlWorkingSpaceClause self)
           
 void visitJmlWorkingSpaceExpression(JmlWorkingSpaceExpression self)
           
 void visitJmlWritableIfVarAssertion(JmlWritableIfVarAssertion self)
           
 
Methods inherited from interface org.multijava.mjc.MjcVisitor
visitAddExpression, visitArrayAccessExpression, visitArrayDimsAndInit, visitArrayInitializer, visitArrayLengthExpression, visitAssertStatement, visitAssignmentExpression, visitBitwiseExpression, visitBlockStatement, visitBooleanLiteral, visitBreakStatement, visitCastExpression, visitCatchClause, visitCharLiteral, visitClassBlock, visitClassDeclaration, visitClassExpression, visitClassOrGFImport, visitCompilationUnit, visitCompoundAssignmentExpression, visitCompoundStatement, visitConditionalAndExpression, visitConditionalExpression, visitConditionalOrExpression, visitConstructorBlock, visitConstructorDeclaration, visitContinueStatement, visitDivideExpression, visitDoStatement, visitEmptyStatement, visitEqualityExpression, visitExplicitConstructorInvocation, visitExpressionListStatement, visitExpressionStatement, visitFieldDeclaration, visitFieldExpression, visitFormalParameters, visitForStatement, visitGenericFunctionDecl, visitIfStatement, visitInitializerDeclaration, visitInstanceofExpression, visitInterfaceDeclaration, visitLabeledStatement, visitLocalVariableExpression, visitMathModeExpression, visitMethodCallExpression, visitMethodDeclaration, visitMinusExpression, visitModuloExpression, visitMultExpression, visitNameExpression, visitNewAnonymousClassExpression, visitNewArrayExpression, visitNewObjectExpression, visitNullLiteral, visitOrdinalLiteral, visitPackageImport, visitPackageName, visitParenthesedExpression, visitPostfixExpression, visitPrefixExpression, visitRealLiteral, visitRelationalExpression, visitReturnStatement, visitShiftExpression, visitStringLiteral, visitSuperExpression, visitSwitchGroup, visitSwitchLabel, visitSwitchStatement, visitSynchronizedStatement, visitThisExpression, visitThrowStatement, visitTopLevelMethodDeclaration, visitTryCatchStatement, visitTryFinallyStatement, visitTypeDeclarationStatement, visitTypeNameExpression, visitUnaryExpression, visitUnaryPromoteExpression, visitVariableDeclarationStatement, visitVariableDefinition, visitWarnExpression, visitWhileStatement
 

Method Detail

visitJmlAbruptSpecBody

public void visitJmlAbruptSpecBody(JmlAbruptSpecBody self)

visitJmlAbruptSpecCase

public void visitJmlAbruptSpecCase(JmlAbruptSpecCase self)

visitJmlAccessibleClause

public void visitJmlAccessibleClause(JmlAccessibleClause self)

visitJmlAssertStatement

public void visitJmlAssertStatement(JmlAssertStatement self)

visitJmlAssignableClause

public void visitJmlAssignableClause(JmlAssignableClause self)

visitJmlAssumeStatement

public void visitJmlAssumeStatement(JmlAssumeStatement self)

visitJmlAxiom

public void visitJmlAxiom(JmlAxiom self)

visitJmlBehaviorSpec

public void visitJmlBehaviorSpec(JmlBehaviorSpec self)

visitJmlBreaksClause

public void visitJmlBreaksClause(JmlBreaksClause self)

visitJmlCallableClause

public void visitJmlCallableClause(JmlCallableClause self)

visitJmlCapturesClause

public void visitJmlCapturesClause(JmlCapturesClause self)

visitJmlClassBlock

public void visitJmlClassBlock(JmlClassBlock self)

visitJmlClassDeclaration

public void visitJmlClassDeclaration(JmlClassDeclaration self)

visitJmlClassOrGFImport

public void visitJmlClassOrGFImport(JmlClassOrGFImport self)

visitJmlCodeContract

public void visitJmlCodeContract(JmlCodeContract self)

visitJmlCompilationUnit

public void visitJmlCompilationUnit(JmlCompilationUnit self)

visitJmlConstraint

public void visitJmlConstraint(JmlConstraint self)

visitJmlConstructorDeclaration

public void visitJmlConstructorDeclaration(JmlConstructorDeclaration self)

visitJmlConstructorName

public void visitJmlConstructorName(JmlConstructorName self)

visitJmlContinuesClause

public void visitJmlContinuesClause(JmlContinuesClause self)

visitJmlDebugStatement

public void visitJmlDebugStatement(JmlDebugStatement self)

visitJmlDeclaration

public void visitJmlDeclaration(JmlDeclaration self)

visitJmlDivergesClause

public void visitJmlDivergesClause(JmlDivergesClause self)

visitJmlDurationClause

public void visitJmlDurationClause(JmlDurationClause self)

visitJmlDurationExpression

public void visitJmlDurationExpression(JmlDurationExpression self)

visitJmlElemTypeExpression

public void visitJmlElemTypeExpression(JmlElemTypeExpression self)

visitJmlEnsuresClause

public void visitJmlEnsuresClause(JmlEnsuresClause self)

visitJmlExample

public void visitJmlExample(JmlExample self)

visitJmlExceptionalBehaviorSpec

public void visitJmlExceptionalBehaviorSpec(JmlExceptionalBehaviorSpec self)

visitJmlExceptionalExample

public void visitJmlExceptionalExample(JmlExceptionalExample self)

visitJmlExceptionalSpecBody

public void visitJmlExceptionalSpecBody(JmlExceptionalSpecBody self)

visitJmlExceptionalSpecCase

public void visitJmlExceptionalSpecCase(JmlExceptionalSpecCase self)

visitJmlExpression

public void visitJmlExpression(JmlExpression self)

visitJmlExtendingSpecification

public void visitJmlExtendingSpecification(JmlExtendingSpecification self)

visitJmlFieldDeclaration

public void visitJmlFieldDeclaration(JmlFieldDeclaration self)

visitJmlForAllVarDecl

public void visitJmlForAllVarDecl(JmlForAllVarDecl self)

visitJmlFormalParameter

public void visitJmlFormalParameter(JmlFormalParameter self)

visitJmlFreshExpression

public void visitJmlFreshExpression(JmlFreshExpression self)

visitJmlGeneralSpecCase

public void visitJmlGeneralSpecCase(JmlGeneralSpecCase self)

visitJmlGenericSpecBody

public void visitJmlGenericSpecBody(JmlGenericSpecBody self)

visitJmlGenericSpecCase

public void visitJmlGenericSpecCase(JmlGenericSpecCase self)

visitJmlGuardedStatement

public void visitJmlGuardedStatement(JmlGuardedStatement self)

visitJmlHenceByStatement

public void visitJmlHenceByStatement(JmlHenceByStatement self)

visitJmlInGroupClause

public void visitJmlInGroupClause(JmlInGroupClause self)

visitJmlInformalExpression

public void visitJmlInformalExpression(JmlInformalExpression self)

visitJmlInformalStoreRef

public void visitJmlInformalStoreRef(JmlInformalStoreRef self)

visitJmlInitiallyVarAssertion

public void visitJmlInitiallyVarAssertion(JmlInitiallyVarAssertion self)

visitJmlInterfaceDeclaration

public void visitJmlInterfaceDeclaration(JmlInterfaceDeclaration self)

visitJmlInvariant

public void visitJmlInvariant(JmlInvariant self)

visitJmlInvariantForExpression

public void visitJmlInvariantForExpression(JmlInvariantForExpression self)

visitJmlInvariantStatement

public void visitJmlInvariantStatement(JmlInvariantStatement self)

visitJmlIsInitializedExpression

public void visitJmlIsInitializedExpression(JmlIsInitializedExpression self)

visitJmlLabelExpression

public void visitJmlLabelExpression(JmlLabelExpression self)

visitJmlLetVarDecl

public void visitJmlLetVarDecl(JmlLetVarDecl self)

visitJmlLockSetExpression

public void visitJmlLockSetExpression(JmlLockSetExpression self)

visitJmlLoopInvariant

public void visitJmlLoopInvariant(JmlLoopInvariant self)

visitJmlLoopStatement

public void visitJmlLoopStatement(JmlLoopStatement self)

visitJmlMapsIntoClause

public void visitJmlMapsIntoClause(JmlMapsIntoClause self)

visitJmlMaxExpression

public void visitJmlMaxExpression(JmlMaxExpression self)

visitJmlMeasuredClause

public void visitJmlMeasuredClause(JmlMeasuredClause self)

visitJmlMethodDeclaration

public void visitJmlMethodDeclaration(JmlMethodDeclaration self)

visitJmlMethodName

public void visitJmlMethodName(JmlMethodName self)

visitJmlMethodNameList

public void visitJmlMethodNameList(JmlMethodNameList self)

visitJmlMethodSpecification

public void visitJmlMethodSpecification(JmlMethodSpecification self)

visitJmlModelProgram

public void visitJmlModelProgram(JmlModelProgram self)

visitJmlMonitorsForVarAssertion

public void visitJmlMonitorsForVarAssertion(JmlMonitorsForVarAssertion self)

visitJmlName

public void visitJmlName(JmlName self)

visitJmlNode

public void visitJmlNode(JmlNode self)

visitJmlNonNullElementsExpression

public void visitJmlNonNullElementsExpression(JmlNonNullElementsExpression self)

visitJmlAssignmentStatement

public void visitJmlAssignmentStatement(JmlAssignmentStatement self)

visitJmlNondetChoiceStatement

public void visitJmlNondetChoiceStatement(JmlNondetChoiceStatement self)

visitJmlNondetIfStatement

public void visitJmlNondetIfStatement(JmlNondetIfStatement self)

visitJmlNormalBehaviorSpec

public void visitJmlNormalBehaviorSpec(JmlNormalBehaviorSpec self)

visitJmlNormalExample

public void visitJmlNormalExample(JmlNormalExample self)

visitJmlNormalSpecBody

public void visitJmlNormalSpecBody(JmlNormalSpecBody self)

visitJmlNormalSpecCase

public void visitJmlNormalSpecCase(JmlNormalSpecCase self)

visitJmlNotAssignedExpression

public void visitJmlNotAssignedExpression(JmlNotAssignedExpression self)

visitJmlNotModifiedExpression

public void visitJmlNotModifiedExpression(JmlNotModifiedExpression self)

visitJmlOnlyAccessedExpression

public void visitJmlOnlyAccessedExpression(JmlOnlyAccessedExpression self)

visitJmlOnlyAssignedExpression

public void visitJmlOnlyAssignedExpression(JmlOnlyAssignedExpression self)

visitJmlOnlyCalledExpression

public void visitJmlOnlyCalledExpression(JmlOnlyCalledExpression self)

visitJmlOnlyCapturedExpression

public void visitJmlOnlyCapturedExpression(JmlOnlyCapturedExpression self)

visitJmlOldExpression

public void visitJmlOldExpression(JmlOldExpression self)

visitJmlPackageImport

public void visitJmlPackageImport(JmlPackageImport self)

visitJmlPredicate

public void visitJmlPredicate(JmlPredicate self)

visitJmlPredicateKeyword

public void visitJmlPredicateKeyword(JmlPredicateKeyword self)

visitJmlPreExpression

public void visitJmlPreExpression(JmlPreExpression self)

visitJmlReachExpression

public void visitJmlReachExpression(JmlReachExpression self)

visitJmlReadableIfVarAssertion

public void visitJmlReadableIfVarAssertion(JmlReadableIfVarAssertion self)

visitJmlWritableIfVarAssertion

public void visitJmlWritableIfVarAssertion(JmlWritableIfVarAssertion self)

visitJmlRedundantSpec

public void visitJmlRedundantSpec(JmlRedundantSpec self)

visitJmlRefinePrefix

public void visitJmlRefinePrefix(JmlRefinePrefix self)

visitJmlRelationalExpression

public void visitJmlRelationalExpression(JmlRelationalExpression self)

visitJmlRepresentsDecl

public void visitJmlRepresentsDecl(JmlRepresentsDecl self)

visitJmlRequiresClause

public void visitJmlRequiresClause(JmlRequiresClause self)

visitJmlResultExpression

public void visitJmlResultExpression(JmlResultExpression self)

visitJmlReturnsClause

public void visitJmlReturnsClause(JmlReturnsClause self)

visitJmlSetComprehension

public void visitJmlSetComprehension(JmlSetComprehension self)

visitJmlSetStatement

public void visitJmlSetStatement(JmlSetStatement self)

visitJmlSignalsOnlyClause

public void visitJmlSignalsOnlyClause(JmlSignalsOnlyClause self)

visitJmlSignalsClause

public void visitJmlSignalsClause(JmlSignalsClause self)

visitJmlSpaceExpression

public void visitJmlSpaceExpression(JmlSpaceExpression self)

visitJmlSpecBody

public void visitJmlSpecBody(JmlSpecBody self)

visitJmlSpecExpression

public void visitJmlSpecExpression(JmlSpecExpression self)

visitJmlSpecQuantifiedExpression

public void visitJmlSpecQuantifiedExpression(JmlSpecQuantifiedExpression self)

visitJmlSpecStatement

public void visitJmlSpecStatement(JmlSpecStatement self)

visitJmlSpecification

public void visitJmlSpecification(JmlSpecification self)

visitJmlSpecVarDecl

public void visitJmlSpecVarDecl(JmlSpecVarDecl self)

visitJmlStoreRef

public void visitJmlStoreRef(JmlStoreRef self)

visitJmlStoreRefExpression

public void visitJmlStoreRefExpression(JmlStoreRefExpression self)

visitJmlStoreRefKeyword

public void visitJmlStoreRefKeyword(JmlStoreRefKeyword self)

visitJmlTypeExpression

public void visitJmlTypeExpression(JmlTypeExpression self)

visitJmlTypeOfExpression

public void visitJmlTypeOfExpression(JmlTypeOfExpression self)

visitJmlUnreachableStatement

public void visitJmlUnreachableStatement(JmlUnreachableStatement self)

visitJmlVariantFunction

public void visitJmlVariantFunction(JmlVariantFunction self)

visitJmlVariableDefinition

public void visitJmlVariableDefinition(JmlVariableDefinition self)

visitJmlWhenClause

public void visitJmlWhenClause(JmlWhenClause self)

visitJmlWorkingSpaceClause

public void visitJmlWorkingSpaceClause(JmlWorkingSpaceClause self)

visitJmlWorkingSpaceExpression

public void visitJmlWorkingSpaceExpression(JmlWorkingSpaceExpression self)

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.