org.jmlspecs.jml4.fspv.simpl.ast
Class SimplWhileStatement

java.lang.Object
  org.jmlspecs.jml4.fspv.simpl.ast.SimplTheoryNode
      org.jmlspecs.jml4.fspv.simpl.ast.SimplStatement
          org.jmlspecs.jml4.fspv.simpl.ast.SimplWhileStatement

public class SimplWhileStatement
extends SimplStatement

Field Summary

SimplStatement	body
SimplExpression	condition
SimplExpression	invariant
SimplExpression	variant

Fields inherited from class org.jmlspecs.jml4.fspv.simpl.ast.SimplStatement

SKIP

Constructor Summary

SimplWhileStatement(SimplExpression condition, SimplStatement body, SimplExpression invariant, SimplExpression variant)

Method Summary

java.lang.String	toString()
java.lang.String	toStringNoAnnotations()

Methods inherited from class java.lang.Object

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

Field Detail

condition

public final SimplExpression condition

body

public final SimplStatement body

invariant

public final SimplExpression invariant

variant

public final SimplExpression variant

Constructor Detail

SimplWhileStatement

public SimplWhileStatement(SimplExpression condition,
                           SimplStatement body,
                           SimplExpression invariant,
                           SimplExpression variant)

Method Detail

toStringNoAnnotations

public java.lang.String toStringNoAnnotations()

toString

public java.lang.String toString()

Overrides:

toString in class java.lang.Object