ESC/Java2
© 2003,2004,2005 David Cok and Joseph Kiniry
© 2005 UCD Dublin
© 2003,2004 Radboud University Nijmegen
© 1999,2000 Compaq Computer Corporation
© 1997,1998,1999 Digital Equipment Corporation
All Rights Reserved

escjava.translate
Class InitialState

java.lang.Object
  extended byescjava.translate.InitialState

public final class InitialState
extends java.lang.Object

This class provides two methods used in the generation of a verification condition for a method or constructor (see section 8 of ESCJ 16).


Field Summary
private  Expr is
           
private  java.util.Hashtable premap
           
 
Constructor Summary
InitialState(FindContributors scope)
           
 
Method Summary
private  VariableAccess addMapping(GenericVarDecl vd)
           
 Expr getInitialState()
           
 java.util.Hashtable getPreMap()
           
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 

Field Detail

premap

private java.util.Hashtable premap

is

private Expr is
Constructor Detail

InitialState

public InitialState(FindContributors scope)
Method Detail

addMapping

private VariableAccess addMapping(GenericVarDecl vd)

getPreMap

public java.util.Hashtable getPreMap()

getInitialState

public Expr getInitialState()

ESC/Java2
© 2003,2004,2005 David Cok and Joseph Kiniry
© 2005 UCD Dublin
© 2003,2004 Radboud University Nijmegen
© 1999,2000 Compaq Computer Corporation
© 1997,1998,1999 Digital Equipment Corporation
All Rights Reserved

The ESC/Java2 Project Homepage