org.jmlspecs.jml4.fspv.theory
Class TheoryWhileStatement

java.lang.Object
  org.jmlspecs.jml4.fspv.theory.TheoryStatement
      org.jmlspecs.jml4.fspv.theory.TheoryWhileStatement

public class TheoryWhileStatement
extends TheoryStatement

Author:

karabot

Field Summary

TheoryBlockStatement	block
TheoryExpression	condition
TheoryLoopAnnotationsExpression	loopAnnotations

Fields inherited from class org.jmlspecs.jml4.fspv.theory.TheoryStatement

EMPTY

Constructor Summary

TheoryWhileStatement(TheoryExpression condition, TheoryLoopAnnotationsExpression loopAnnotations, TheoryBlockStatement block)

Method Summary

java.lang.Object

visit(TheoryVisitor visitor)

Methods inherited from class java.lang.Object

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

Field Detail

condition

public final TheoryExpression condition

loopAnnotations

public final TheoryLoopAnnotationsExpression loopAnnotations

block

public final TheoryBlockStatement block

Constructor Detail

TheoryWhileStatement

public TheoryWhileStatement(TheoryExpression condition,
                            TheoryLoopAnnotationsExpression loopAnnotations,
                            TheoryBlockStatement block)

Method Detail

visit

public java.lang.Object visit(TheoryVisitor visitor)

Overrides:

visit in class TheoryStatement