Overview  Package   Class  Use  Tree  Deprecated  Index  Help 
 PREV CLASS   NEXT CLASS FRAMES    NO FRAMES    
SUMMARY: NESTED | FIELD | CONSTR | METHOD DETAIL: FIELD | CONSTR | METHOD

org.jmlspecs.jml4.fspv.phases
Class TheoryTranslation

java.lang.Object
  extended by org.eclipse.jdt.internal.compiler.ASTVisitor
      extended by org.jmlspecs.jml4.fspv.TraceAstVisitor
          extended by org.jmlspecs.jml4.fspv.phases.TheoryTranslation

public class TheoryTranslation
extends TraceAstVisitor

Field Summary
 Theory theory
           
 
Constructor Summary
TheoryTranslation()
           
 
Method Summary
 void endVisit(AllocationExpression allocationExpression, BlockScope scope)
           
 void endVisit(Argument argument, BlockScope scope)
           
 void endVisit(Assignment assignment, BlockScope scope)
           
 void endVisit(BinaryExpression binaryExpression, BlockScope scope)
           
 void endVisit(Block block, BlockScope scope)
           
 void endVisit(CompilationUnitDeclaration compilationUnitDeclaration, CompilationUnitScope scope)
           
 void endVisit(CompoundAssignment compoundAssignment, BlockScope scope)
           
 void endVisit(ConstructorDeclaration constructorDeclaration, ClassScope scope)
           
 void endVisit(EqualExpression equalExpression, BlockScope scope)
           
 void endVisit(ExplicitConstructorCall explicitConstructor, BlockScope scope)
           
 void endVisit(FalseLiteral falseLiteral, BlockScope scope)
           
 void endVisit(FieldDeclaration fieldDeclaration, MethodScope scope)
           
 void endVisit(IntLiteral intLiteral, BlockScope scope)
           
 void endVisit(JmlAssignment assignment, BlockScope scope)
           
 void endVisit(JmlClause jmlClause, BlockScope scope)
           
 void endVisit(JmlCompilationUnitDeclaration compilationUnitDeclaration, CompilationUnitScope scope)
           
 void endVisit(JmlConstructorDeclaration constructorDeclaration, ClassScope scope)
           
 void endVisit(JmlLoopAnnotations jmlLoopAnnotations, BlockScope scope)
           
 void endVisit(JmlLoopInvariant jmlLoopInvariant, BlockScope scope)
           
 void endVisit(JmlLoopVariant jmlLoopVariant, BlockScope scope)
           
 void endVisit(JmlMethodDeclaration methodDeclaration, ClassScope scope)
           
 void endVisit(JmlOldExpression jmlOldExpression, BlockScope scope)
           
 void endVisit(JmlResultReference resultReference, BlockScope scope)
           
 void endVisit(JmlWhileStatement whileStatement, BlockScope scope)
           
 void endVisit(LocalDeclaration localDeclaration, BlockScope scope)
           
 void endVisit(MessageSend messageSend, BlockScope scope)
           
 void endVisit(MethodDeclaration methodDeclaration, ClassScope scope)
           
 void endVisit(NullLiteral nullLiteral, BlockScope scope)
           
 void endVisit(PostfixExpression postfixExpression, BlockScope scope)
           
 void endVisit(ReturnStatement returnStatement, BlockScope scope)
           
 void endVisit(SingleNameReference singleNameReference, BlockScope scope)
           
 void endVisit(SingleTypeReference singleTypeReference, BlockScope scope)
           
 void endVisit(TrueLiteral trueLiteral, BlockScope scope)
           
 void endVisit(TypeDeclaration typeDeclaration, CompilationUnitScope scope)
           
 boolean visit(AllocationExpression allocationExpression, BlockScope scope)
           
 boolean visit(Argument argument, BlockScope scope)
           
 boolean visit(Assignment assignment, BlockScope scope)
           
 boolean visit(BinaryExpression binaryExpression, BlockScope scope)
           
 boolean visit(Block block, BlockScope scope)
           
 boolean visit(CompilationUnitDeclaration compilationUnitDeclaration, CompilationUnitScope scope)
           
 boolean visit(CompoundAssignment compoundAssignment, BlockScope scope)
           
 boolean visit(ConstructorDeclaration constructorDeclaration, ClassScope scope)
           
 boolean visit(EqualExpression equalExpression, BlockScope scope)
           
 boolean visit(ExplicitConstructorCall explicitConstructor, BlockScope scope)
           
 boolean visit(FalseLiteral falseLiteral, BlockScope scope)
           
 boolean visit(FieldDeclaration fieldDeclaration, MethodScope scope)
           
 boolean visit(FieldReference fieldReference, BlockScope scope)
           
 boolean visit(IntLiteral intLiteral, BlockScope scope)
           
 boolean visit(JmlAssignment assignment, BlockScope scope)
           
 boolean visit(JmlClause jmlClause, BlockScope scope)
           
 boolean visit(JmlCompilationUnitDeclaration compilationUnitDeclaration, CompilationUnitScope scope)
           
 boolean visit(JmlConstructorDeclaration constructorDeclaration, ClassScope scope)
           
 boolean visit(JmlLoopAnnotations jmlLoopAnnotations, BlockScope scope)
           
 boolean visit(JmlLoopInvariant jmlLoopInvariant, BlockScope scope)
           
 boolean visit(JmlLoopVariant jmlLoopVariant, BlockScope scope)
           
 boolean visit(JmlMethodDeclaration methodDeclaration, ClassScope scope)
           
 boolean visit(JmlOldExpression jmlOldExpression, BlockScope scope)
           
 boolean visit(JmlResultReference resultReference, BlockScope scope)
           
 boolean visit(JmlWhileStatement whileStatement, BlockScope scope)
           
 boolean visit(LocalDeclaration localDeclaration, BlockScope scope)
           
 boolean visit(MessageSend messageSend, BlockScope scope)
           
 boolean visit(MethodDeclaration methodDeclaration, ClassScope scope)
           
 boolean visit(NullLiteral nullLiteral, BlockScope scope)
           
 boolean visit(PostfixExpression postfixExpression, BlockScope scope)
           
 boolean visit(ReturnStatement returnStatement, BlockScope scope)
           
 boolean visit(SingleNameReference singleNameReference, BlockScope scope)
           
 boolean visit(SingleTypeReference singleTypeReference, BlockScope scope)
           
 boolean visit(TrueLiteral trueLiteral, BlockScope scope)
           
 boolean visit(TypeDeclaration typeDeclaration, CompilationUnitScope scope)
           
 
Methods inherited from class org.jmlspecs.jml4.fspv.TraceAstVisitor
acceptProblem, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit
 
Methods inherited from class org.eclipse.jdt.internal.compiler.ASTVisitor
endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, endVisit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit, visit
 
Methods inherited from class java.lang.Object
equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 

Field Detail

theory

public Theory theory
Constructor Detail

TheoryTranslation

public TheoryTranslation()
Method Detail

visit

public boolean visit(JmlCompilationUnitDeclaration compilationUnitDeclaration,
                     CompilationUnitScope scope)
Overrides:
visit in class TraceAstVisitor

endVisit

public void endVisit(JmlCompilationUnitDeclaration compilationUnitDeclaration,
                     CompilationUnitScope scope)
Overrides:
endVisit in class TraceAstVisitor

visit

public boolean visit(CompilationUnitDeclaration compilationUnitDeclaration,
                     CompilationUnitScope scope)
Overrides:
visit in class TraceAstVisitor

endVisit

public void endVisit(CompilationUnitDeclaration compilationUnitDeclaration,
                     CompilationUnitScope scope)
Overrides:
endVisit in class TraceAstVisitor

visit

public boolean visit(SingleTypeReference singleTypeReference,
                     BlockScope scope)
Overrides:
visit in class TraceAstVisitor

endVisit

public void endVisit(SingleTypeReference singleTypeReference,
                     BlockScope scope)
Overrides:
endVisit in class TraceAstVisitor

visit

public boolean visit(TypeDeclaration typeDeclaration,
                     CompilationUnitScope scope)
Overrides:
visit in class TraceAstVisitor

endVisit

public void endVisit(TypeDeclaration typeDeclaration,
                     CompilationUnitScope scope)
Overrides:
endVisit in class TraceAstVisitor

visit

public boolean visit(JmlConstructorDeclaration constructorDeclaration,
                     ClassScope scope)
Overrides:
visit in class TraceAstVisitor

endVisit

public void endVisit(JmlConstructorDeclaration constructorDeclaration,
                     ClassScope scope)
Overrides:
endVisit in class TraceAstVisitor

visit

public boolean visit(ConstructorDeclaration constructorDeclaration,
                     ClassScope scope)
Overrides:
visit in class TraceAstVisitor

endVisit

public void endVisit(ConstructorDeclaration constructorDeclaration,
                     ClassScope scope)
Overrides:
endVisit in class TraceAstVisitor

visit

public boolean visit(FieldDeclaration fieldDeclaration,
                     MethodScope scope)
Overrides:
visit in class TraceAstVisitor

endVisit

public void endVisit(FieldDeclaration fieldDeclaration,
                     MethodScope scope)
Overrides:
endVisit in class TraceAstVisitor

visit

public boolean visit(JmlMethodDeclaration methodDeclaration,
                     ClassScope scope)
Overrides:
visit in class TraceAstVisitor

endVisit

public void endVisit(JmlMethodDeclaration methodDeclaration,
                     ClassScope scope)
Overrides:
endVisit in class TraceAstVisitor

visit

public boolean visit(MethodDeclaration methodDeclaration,
                     ClassScope scope)
Overrides:
visit in class TraceAstVisitor

endVisit

public void endVisit(MethodDeclaration methodDeclaration,
                     ClassScope scope)
Overrides:
endVisit in class TraceAstVisitor

visit

public boolean visit(Argument argument,
                     BlockScope scope)
Overrides:
visit in class TraceAstVisitor

endVisit

public void endVisit(Argument argument,
                     BlockScope scope)
Overrides:
endVisit in class TraceAstVisitor

visit

public boolean visit(Block block,
                     BlockScope scope)
Overrides:
visit in class TraceAstVisitor

endVisit

public void endVisit(Block block,
                     BlockScope scope)
Overrides:
endVisit in class TraceAstVisitor

visit

public boolean visit(LocalDeclaration localDeclaration,
                     BlockScope scope)
Overrides:
visit in class TraceAstVisitor

endVisit

public void endVisit(LocalDeclaration localDeclaration,
                     BlockScope scope)
Overrides:
endVisit in class TraceAstVisitor

visit

public boolean visit(ReturnStatement returnStatement,
                     BlockScope scope)
Overrides:
visit in class TraceAstVisitor

endVisit

public void endVisit(ReturnStatement returnStatement,
                     BlockScope scope)
Overrides:
endVisit in class TraceAstVisitor

visit

public boolean visit(ExplicitConstructorCall explicitConstructor,
                     BlockScope scope)
Overrides:
visit in class TraceAstVisitor

endVisit

public void endVisit(ExplicitConstructorCall explicitConstructor,
                     BlockScope scope)
Overrides:
endVisit in class TraceAstVisitor

visit

public boolean visit(JmlWhileStatement whileStatement,
                     BlockScope scope)
Overrides:
visit in class TraceAstVisitor

endVisit

public void endVisit(JmlWhileStatement whileStatement,
                     BlockScope scope)
Overrides:
endVisit in class TraceAstVisitor

visit

public boolean visit(AllocationExpression allocationExpression,
                     BlockScope scope)
Overrides:
visit in class TraceAstVisitor

endVisit

public void endVisit(AllocationExpression allocationExpression,
                     BlockScope scope)
Overrides:
endVisit in class TraceAstVisitor

visit

public boolean visit(JmlAssignment assignment,
                     BlockScope scope)
Overrides:
visit in class TraceAstVisitor

endVisit

public void endVisit(JmlAssignment assignment,
                     BlockScope scope)
Overrides:
endVisit in class TraceAstVisitor

visit

public boolean visit(Assignment assignment,
                     BlockScope scope)
Overrides:
visit in class TraceAstVisitor

endVisit

public void endVisit(Assignment assignment,
                     BlockScope scope)
Overrides:
endVisit in class TraceAstVisitor

visit

public boolean visit(BinaryExpression binaryExpression,
                     BlockScope scope)
Overrides:
visit in class TraceAstVisitor

endVisit

public void endVisit(BinaryExpression binaryExpression,
                     BlockScope scope)
Overrides:
endVisit in class TraceAstVisitor

visit

public boolean visit(CompoundAssignment compoundAssignment,
                     BlockScope scope)
Overrides:
visit in class TraceAstVisitor

endVisit

public void endVisit(CompoundAssignment compoundAssignment,
                     BlockScope scope)
Overrides:
endVisit in class TraceAstVisitor

visit

public boolean visit(EqualExpression equalExpression,
                     BlockScope scope)
Overrides:
visit in class TraceAstVisitor

endVisit

public void endVisit(EqualExpression equalExpression,
                     BlockScope scope)
Overrides:
endVisit in class TraceAstVisitor

visit

public boolean visit(MessageSend messageSend,
                     BlockScope scope)
Overrides:
visit in class TraceAstVisitor

endVisit

public void endVisit(MessageSend messageSend,
                     BlockScope scope)
Overrides:
endVisit in class TraceAstVisitor

visit

public boolean visit(PostfixExpression postfixExpression,
                     BlockScope scope)
Overrides:
visit in class TraceAstVisitor

endVisit

public void endVisit(PostfixExpression postfixExpression,
                     BlockScope scope)
Overrides:
endVisit in class TraceAstVisitor

visit

public boolean visit(SingleNameReference singleNameReference,
                     BlockScope scope)
Overrides:
visit in class TraceAstVisitor

endVisit

public void endVisit(SingleNameReference singleNameReference,
                     BlockScope scope)
Overrides:
endVisit in class TraceAstVisitor

visit

public boolean visit(FieldReference fieldReference,
                     BlockScope scope)
Overrides:
visit in class TraceAstVisitor

visit

public boolean visit(IntLiteral intLiteral,
                     BlockScope scope)
Overrides:
visit in class TraceAstVisitor

endVisit

public void endVisit(IntLiteral intLiteral,
                     BlockScope scope)
Overrides:
endVisit in class TraceAstVisitor

visit

public boolean visit(TrueLiteral trueLiteral,
                     BlockScope scope)
Overrides:
visit in class TraceAstVisitor

endVisit

public void endVisit(TrueLiteral trueLiteral,
                     BlockScope scope)
Overrides:
endVisit in class TraceAstVisitor

visit

public boolean visit(FalseLiteral falseLiteral,
                     BlockScope scope)
Overrides:
visit in class TraceAstVisitor

endVisit

public void endVisit(FalseLiteral falseLiteral,
                     BlockScope scope)
Overrides:
endVisit in class TraceAstVisitor

visit

public boolean visit(NullLiteral nullLiteral,
                     BlockScope scope)
Overrides:
visit in class TraceAstVisitor

endVisit

public void endVisit(NullLiteral nullLiteral,
                     BlockScope scope)
Overrides:
endVisit in class TraceAstVisitor

visit

public boolean visit(JmlClause jmlClause,
                     BlockScope scope)
Overrides:
visit in class TraceAstVisitor

endVisit

public void endVisit(JmlClause jmlClause,
                     BlockScope scope)
Overrides:
endVisit in class TraceAstVisitor

visit

public boolean visit(JmlLoopAnnotations jmlLoopAnnotations,
                     BlockScope scope)
Overrides:
visit in class TraceAstVisitor

endVisit

public void endVisit(JmlLoopAnnotations jmlLoopAnnotations,
                     BlockScope scope)
Overrides:
endVisit in class TraceAstVisitor

visit

public boolean visit(JmlLoopInvariant jmlLoopInvariant,
                     BlockScope scope)
Overrides:
visit in class TraceAstVisitor

endVisit

public void endVisit(JmlLoopInvariant jmlLoopInvariant,
                     BlockScope scope)
Overrides:
endVisit in class TraceAstVisitor

visit

public boolean visit(JmlLoopVariant jmlLoopVariant,
                     BlockScope scope)
Overrides:
visit in class TraceAstVisitor

endVisit

public void endVisit(JmlLoopVariant jmlLoopVariant,
                     BlockScope scope)
Overrides:
endVisit in class TraceAstVisitor

visit

public boolean visit(JmlOldExpression jmlOldExpression,
                     BlockScope scope)
Overrides:
visit in class TraceAstVisitor

endVisit

public void endVisit(JmlOldExpression jmlOldExpression,
                     BlockScope scope)
Overrides:
endVisit in class TraceAstVisitor

visit

public boolean visit(JmlResultReference resultReference,
                     BlockScope scope)
Overrides:
visit in class TraceAstVisitor

endVisit

public void endVisit(JmlResultReference resultReference,
                     BlockScope scope)
Overrides:
endVisit in class TraceAstVisitor
Overview  Package   Class  Use  Tree  Deprecated  Index  Help 
 PREV CLASS   NEXT CLASS FRAMES    NO FRAMES    
SUMMARY: NESTED | FIELD | CONSTR | METHOD DETAIL: FIELD | CONSTR | METHOD