org.jmlspecs.jml4.fspv
Class PrestateDecorator

java.lang.Object
  org.jmlspecs.jml4.fspv.theory.TheoryVisitor
      org.jmlspecs.jml4.fspv.PrestateDecorator

public class PrestateDecorator
extends TheoryVisitor

Constructor Summary

PrestateDecorator()

Method Summary

java.lang.Object	accept(Theory theory)
java.lang.Object	accept(TheoryAssignmentStatement theoryAssignmentStatement)
java.lang.Object	accept(TheoryBinaryExpression theoryBinaryExpression)
java.lang.Object	accept(TheoryBlockStatement theoryBlockStatement)
java.lang.Object	accept(TheoryConditionalStatement theoryConditionalStatement)
java.lang.Object	accept(TheoryInvariantExpression theoryInvariantExpression)
java.lang.Object	accept(TheoryLemma lemma)
java.lang.Object	accept(TheoryLiteral theoryLiteral)
java.lang.Object	accept(TheoryLocalDeclarationBlockStatement theoryLocalDeclarationBlockStatement)
java.lang.Object	accept(TheoryLoopAnnotationsExpression theoryLoopAnnotationsExpression)
java.lang.Object	accept(TheoryOldExpression theoryOldExpression)
java.lang.Object	accept(TheoryQuantifiedExpression theoryQuantifiedExpression)
java.lang.Object	accept(TheoryVariable theoryVariable)
java.lang.Object	accept(TheoryVariableReference theoryVariableReference)
java.lang.Object	accept(TheoryVariantExpression theoryVariantExpression)
java.lang.Object	accept(TheoryWhileStatement theoryWhileStatement)

Methods inherited from class org.jmlspecs.jml4.fspv.theory.TheoryVisitor

accept, accept, accept, accept, accept, accept, accept, accept, accept, accept

Methods inherited from class java.lang.Object

equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

PrestateDecorator

public PrestateDecorator()

Method Detail

accept

public java.lang.Object accept(Theory theory)

Overrides:

accept in class TheoryVisitor

accept

public java.lang.Object accept(TheoryLemma lemma)

Overrides:

accept in class TheoryVisitor

accept

public java.lang.Object accept(TheoryVariable theoryVariable)

Overrides:

accept in class TheoryVisitor

accept

public java.lang.Object accept(TheoryAssignmentStatement theoryAssignmentStatement)

Overrides:

accept in class TheoryVisitor

accept

public java.lang.Object accept(TheoryConditionalStatement theoryConditionalStatement)

Overrides:

accept in class TheoryVisitor

accept

public java.lang.Object accept(TheoryWhileStatement theoryWhileStatement)

Overrides:

accept in class TheoryVisitor

accept

public java.lang.Object accept(TheoryBlockStatement theoryBlockStatement)

Overrides:

accept in class TheoryVisitor

accept

public java.lang.Object accept(TheoryLocalDeclarationBlockStatement theoryLocalDeclarationBlockStatement)

Overrides:

accept in class TheoryVisitor

accept

public java.lang.Object accept(TheoryLoopAnnotationsExpression theoryLoopAnnotationsExpression)

Overrides:

accept in class TheoryVisitor

accept

public java.lang.Object accept(TheoryVariantExpression theoryVariantExpression)

Overrides:

accept in class TheoryVisitor

accept

public java.lang.Object accept(TheoryInvariantExpression theoryInvariantExpression)

Overrides:

accept in class TheoryVisitor

accept

public java.lang.Object accept(TheoryBinaryExpression theoryBinaryExpression)

Overrides:

accept in class TheoryVisitor

accept

public java.lang.Object accept(TheoryLiteral theoryLiteral)

Overrides:

accept in class TheoryVisitor

accept

public java.lang.Object accept(TheoryVariableReference theoryVariableReference)

Overrides:

accept in class TheoryVisitor

accept

public java.lang.Object accept(TheoryOldExpression theoryOldExpression)

Overrides:

accept in class TheoryVisitor

accept

public java.lang.Object accept(TheoryQuantifiedExpression theoryQuantifiedExpression)

Overrides:

accept in class TheoryVisitor