org.jmlspecs.jml4.fspv.theory.ast
Class TheoryWhileStatement

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

public class TheoryWhileStatement
extends TheoryStatement

Field Summary

TheoryStatement	action
TheoryExpression	condition
TheoryExpression[]	invariants
TheoryExpression[]	variants

Fields inherited from class org.jmlspecs.jml4.fspv.theory.ast.TheoryNode

base, enclosingTheory

Constructor Summary

TheoryWhileStatement(ASTNode base, Theory theory, TheoryExpression condition, TheoryStatement action, TheoryExpression[] invariants, TheoryExpression[] variants)

Method Summary

void	traverse(TheoryVisitor visitor)

Methods inherited from class org.jmlspecs.jml4.fspv.theory.ast.TheoryNode

toString

Methods inherited from class java.lang.Object

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

Field Detail

condition

public final TheoryExpression condition

action

public final TheoryStatement action

invariants

public final TheoryExpression[] invariants

variants

public final TheoryExpression[] variants

Constructor Detail

TheoryWhileStatement

public TheoryWhileStatement(ASTNode base,
                            Theory theory,
                            TheoryExpression condition,
                            TheoryStatement action,
                            TheoryExpression[] invariants,
                            TheoryExpression[] variants)

Method Detail

traverse

public void traverse(TheoryVisitor visitor)

Specified by:

traverse in class TheoryNode