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

java.lang.Object
  org.jmlspecs.jml4.fspv.simpl.ast.SimplTheoryNode
      org.jmlspecs.jml4.fspv.simpl.ast.SimplStatement
          org.jmlspecs.jml4.fspv.simpl.ast.SimplExpression
              org.jmlspecs.jml4.fspv.simpl.ast.SimplVariableReference
                  org.jmlspecs.jml4.fspv.simpl.ast.SimplPrestateVariableReference

public class SimplPrestateVariableReference
extends SimplVariableReference

Field Summary

java.lang.String

prestateVariable

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

name

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

RESULT, THIS, THIS_EQUAL_PRE_THIS, THIS_NOT_NULL

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

SKIP

Constructor Summary

SimplPrestateVariableReference(java.lang.String name, java.lang.String prestateVariable)

Method Summary

java.lang.String

toString()

Methods inherited from class java.lang.Object

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

Field Detail

prestateVariable

public final java.lang.String prestateVariable

Constructor Detail

SimplPrestateVariableReference

public SimplPrestateVariableReference(java.lang.String name,
                                      java.lang.String prestateVariable)

Method Detail

toString

public java.lang.String toString()

Overrides:

toString in class SimplVariableReference