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	visitJmlOtherRef(JmlOtherRef 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)

visitJmlOtherRef

public void visitJmlOtherRef(JmlOtherRef 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)