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
Class TheoryTranslator

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

public class TheoryTranslator
extends TraceAstVisitor

Field Summary
 TheoryHelper helper
           
 Theory theory
           
 
Constructor Summary
TheoryTranslator()
           
 
Method Summary
 void endVisit(AND_AND_Expression and_and_Expression, 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(EqualExpression equalExpression, BlockScope scope)
           
 void endVisit(FalseLiteral falseLiteral, BlockScope scope)
           
 void endVisit(IfStatement ifStatement, BlockScope 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(JmlLoopAnnotations jmlLoopAnnotations, BlockScope scope)
           
 void endVisit(JmlLoopInvariant jmlLoopInvariant, BlockScope scope)
           
 void endVisit(JmlLoopVariant jmlLoopVariant, BlockScope scope)
           
 void endVisit(JmlMethodDeclaration methodDeclaration, ClassScope scope)
           
 void endVisit(JmlQuantifiedExpression expr, BlockScope scope)
           
 void endVisit(JmlResultReference resultReference, BlockScope scope)
           
 void endVisit(JmlWhileStatement whileStatement, BlockScope scope)
           
 void endVisit(LocalDeclaration localDeclaration, BlockScope scope)
           
 void endVisit(MethodDeclaration methodDeclaration, ClassScope scope)
           
 void endVisit(OR_OR_Expression or_or_Expression, BlockScope scope)
           
 void endVisit(PostfixExpression postfixExpression, BlockScope scope)
           
 void endVisit(PrefixExpression prefixExpression, 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)
           
 void endVisit(UnaryExpression unaryExpression, BlockScope scope)
           
 boolean visit(AND_AND_Expression and_and_Expression, 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(EqualExpression equalExpression, BlockScope scope)
           
 boolean visit(FalseLiteral falseLiteral, BlockScope scope)
           
 boolean visit(IfStatement ifStatement, 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(JmlLoopAnnotations jmlLoopAnnotations, BlockScope scope)
           
 boolean visit(JmlLoopInvariant jmlLoopInvariant, BlockScope scope)
           
 boolean visit(JmlLoopVariant jmlLoopVariant, BlockScope scope)
           
 boolean visit(JmlMethodDeclaration methodDeclaration, ClassScope scope)
           
 boolean visit(JmlQuantifiedExpression expr, BlockScope scope)
           
 boolean visit(JmlResultReference resultReference, BlockScope scope)
           
 boolean visit(JmlWhileStatement whileStatement, BlockScope scope)
           
 boolean visit(LocalDeclaration localDeclaration, BlockScope scope)
           
 boolean visit(MethodDeclaration methodDeclaration, ClassScope scope)
           
 boolean visit(OR_OR_Expression or_or_Expression, BlockScope scope)
           
 boolean visit(PostfixExpression postfixExpression, BlockScope scope)
           
 boolean visit(PrefixExpression prefixExpression, 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)
           
 boolean visit(UnaryExpression unaryExpression, BlockScope scope)
           
 boolean visit(WhileStatement whileStatement, BlockScope 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, 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, 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

helper

public TheoryHelper helper
Constructor Detail

TheoryTranslator

public TheoryTranslator()
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(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(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(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(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(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(IfStatement ifStatement,
                     BlockScope scope)
Overrides:
visit in class TraceAstVisitor

endVisit

public void endVisit(IfStatement ifStatement,
                     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(WhileStatement whileStatement,
                     BlockScope scope)
Overrides:
visit 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(PrefixExpression prefixExpression,
                     BlockScope scope)
Overrides:
visit in class TraceAstVisitor

endVisit

public void endVisit(PrefixExpression prefixExpression,
                     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(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(AND_AND_Expression and_and_Expression,
                     BlockScope scope)
Overrides:
visit in class TraceAstVisitor

endVisit

public void endVisit(AND_AND_Expression and_and_Expression,
                     BlockScope scope)
Overrides:
endVisit in class TraceAstVisitor

visit

public boolean visit(OR_OR_Expression or_or_Expression,
                     BlockScope scope)
Overrides:
visit in class TraceAstVisitor

endVisit

public void endVisit(OR_OR_Expression or_or_Expression,
                     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(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(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(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(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(JmlQuantifiedExpression expr,
                     BlockScope scope)
Overrides:
visit in class TraceAstVisitor

endVisit

public void endVisit(JmlQuantifiedExpression expr,
                     BlockScope scope)
Overrides:
endVisit in class TraceAstVisitor

visit

public boolean visit(UnaryExpression unaryExpression,
                     BlockScope scope)
Overrides:
visit in class TraceAstVisitor

endVisit

public void endVisit(UnaryExpression unaryExpression,
                     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

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(JmlClause jmlClause,
                     BlockScope scope)
Overrides:
visit in class TraceAstVisitor

endVisit

public void endVisit(JmlClause jmlClause,
                     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